Natarajan Shankar

Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

2021

2018 CAV award.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

Semantic parsing of geometry statements using supervised machine learning on synthetic data.

[BibT_eX]

[DOI]

Salwa Tabet Gonzalez

Julien Narboux

Proceedings of the Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26, 2021

The Verified Software Initiative: A Manifesto.

[BibT_eX]

[DOI]

Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

The First Fifteen Years of the Verified Software Project.

[BibT_eX]

[DOI]

Peter Müller

Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

2020

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness.

[BibT_eX]

[DOI]

Maria Paola Bonacina

J. Autom. Reason., 2020

The Correctness of a Code Generator for a Functional Language.

[BibT_eX]

[DOI]

Nathanaël Courant

Antoine Séré

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Research Report: The Parsley Data Format Definition Language.

[BibT_eX]

[DOI]

Prashanth Mundkur

Linda Briesemeister

Prashant Anantharaman

Sameed Ali

Zephyr Lucas

Sean W. Smith

Proceedings of the 2020 IEEE Security and Privacy Workshops, 2020

Model-Centered Assurance for Autonomous Systems.

[BibT_eX]

[DOI]

Susmit Jha

John Rushby

Proceedings of the Computer Safety, Reliability, and Security, 2020

A verified packrat parser interpreter for parsing expression grammars.

[BibT_eX]

[DOI]

Clement Blaudeau

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

TeLEx: learning signal temporal logic from positive examples using tightness metric.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2019

SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems.

[BibT_eX]

[DOI]

Proceedings of the 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2019

A Refinement Proof for a Garbage Collector.

[BibT_eX]

[DOI]

Klaus Havelund

Proceedings of the From Reactive Systems to Cyber-Physical Systems, 2019

2018

Combining Model Checking and Deduction.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Model Checking., 2018

Alonzo Church Award 2018 - Call for Nominations.

[BibT_eX]

[DOI]

Bull. EATCS, 2018

SOTER: Programming Safe Robotics System using Runtime Assurance.

[BibT_eX]

[DOI]

CoRR, 2018

Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2018

Proofs in conflict-driven theory combination.

[BibT_eX]

[DOI]

Maria Paola Bonacina

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Alonzo Church Award 2017 - Call for Nominations.

[BibT_eX]

[DOI]

Bull. EATCS, 2017

Formalizing Hoare Logic in PVS.

[BibT_eX]

[DOI]

Proceedings of the Engineering Trustworthy Software Systems - Third International School, 2017

TeLEx: Passive STL Learning Using Only Positive Examples.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 17th International Conference, 2017

A Brief Introduction to the PVS2C Code Generator.

[BibT_eX]

[DOI]

Proceedings of the Automated Formal Methods, 2017

Satisfiability Modulo Theories and Assignments.

[BibT_eX]

[DOI]

Maria Paola Bonacina

Proceedings of the Automated Deduction - CADE 26, 2017

2016

ARSENAL: Automatic Requirements Specification Extraction from Natural Language.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Code Generation Using a Formal Model of Reference Counting.

[BibT_eX]

[DOI]

Gaspard Férey

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems.

[BibT_eX]

[DOI]

Devesh Bhatt

Arunabh Chattopadhyay

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Double Helix and RAVEN: A System for Cyber Fault Tolerance and Recovery.

[BibT_eX]

[DOI]

Proceedings of the 11th Annual Cyber and Information Security Research Conference, 2016

2015

Identifying Negative Cost Cycles in Strongly Polynomial Space.

[BibT_eX]

K. Subramani

Pavlos Eirinakis

Nord. J. Comput., 2015

Automated software winnowing.

[BibT_eX]

[DOI]

Gregory Malecha

Ashish Gehani

Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015

Design and verification of multi-rate distributed systems.

[BibT_eX]

[DOI]

Wenchao Li

Léonard Gérard

Proceedings of the 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2015

Design and verification for transportation system security.

[BibT_eX]

[DOI]

Proceedings of the 52nd Annual Design Automation Conference, 2015

2014

Reverse Engineering Digital Circuits Using Structural and Functional Analyses.

[BibT_eX]

[DOI]

IEEE Trans. Emerg. Top. Comput., 2014

Automatically Extracting Requirements Specifications from Natural Language.

[BibT_eX]

[DOI]

CoRR, 2014

The Gradual Verifier.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

A framework for high-assurance quasi-synchronous systems.

[BibT_eX]

[DOI]

Robin Larrieu

Proceedings of the Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2014

Software engineering and automated deduction.

[BibT_eX]

[DOI]

Willem Visser

Nikolaj S. Bjørner

Proceedings of the on Future of Software Engineering, 2014

The Semantics of Datalog for the Evidential Tool Bus - (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Specification, Algebra, and Software, 2014

2013

EFSMT: A Logical Framework for Cyber-Physical Systems.

[BibT_eX]

[DOI]

CoRR, 2013

Tool Integration with the Evidential Tool Bus.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2013

WordRev: Finding word-level structures in a sea of bit-level gates.

[BibT_eX]

[DOI]

Proceedings of the 2013 IEEE International Symposium on Hardware-Oriented Security and Trust, 2013

JBernstein: A Validity Checker for Generalized Polynomial Constraints.

[BibT_eX]

[DOI]

Chih-Hong Cheng

Harald Ruess

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Automated Reasoning, Fast and Slow.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

2012

ModelRob: A Simulink Library for Model-Based Development of robot manipulators.

[BibT_eX]

[DOI]

Indranil Saha

Proceedings of the IEEE International Conference on Robotics and Automation, 2012

Automatic Dimensional Analysis of Cyber-Physical Systems.

[BibT_eX]

[DOI]

Indranil Saha

Proceedings of the FM 2012: Formal Methods, 2012

The Architecture of Inference from SMT to ETB.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011

A mechanical verification of the stressing algorithm for negative cost cycle detection in networks.

[BibT_eX]

[DOI]

K. Subramani

Sci. Comput. Program., 2011

SimCheck: a contract type system for Simulink.

[BibT_eX]

[DOI]

Pritam Roy

Innov. Syst. Softw. Eng., 2011

The 1st Verified Software Competition: Experience Report.

[BibT_eX]

[DOI]

Proceedings of the FM 2011: Formal Methods, 2011

Solving the First Verified Software Competition Problems Using PVS.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling: Actors, Open Systems, Biological Systems, 2011

2010

The Mechanical Verification of a DPLL-Based Satisfiability Solver.

[BibT_eX]

[DOI]

Marc Vaucher

Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop, 2010

Rewriting, Inference, and Proof.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

SimCheck: An Expressive Type System for Simulink.

[BibT_eX]

Pritam Roy

Proceedings of the Second NASA Formal Methods Symposium, 2010

Unraveling a Card Trick.

[BibT_eX]

[DOI]

Tony Hoare

Proceedings of the Time for Verification, 2010

2009

Automated deduction for verification.

[BibT_eX]

[DOI]

ACM Comput. Surv., 2009

The verified software initiative: A manifesto.

[BibT_eX]

[DOI]

ACM Comput. Surv., 2009

System Support for Forensic Inference.

[BibT_eX]

[DOI]

Ashish Gehani

Florent Kirchner

Proceedings of the Advances in Digital Forensics V, 2009

2008

A Brief Overview of PVS.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Fixpoints and Search in PVS.

[BibT_eX]

[DOI]

Proceedings of the Advanced Lectures on Software Engineering, 2008

Trust and Automation in Verification Tools.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

A Tutorial on Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Bruno Dutertre

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2005

Inference Systems for Logical Algorithms.

[BibT_eX]

[DOI]

Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004

Justifying Equality.

[BibT_eX]

[DOI]

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

SAL 2.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

The ICS Decision Procedures for Embedded Deduction.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Invisible formal methods for embedded control systems.

[BibT_eX]

[DOI]

Ashish Tiwari

Proc. IEEE, 2003

2002

Verification by Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods at the Crossroads. From Panacea to Foundational Support, 2002

Combining Shostak Theories.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 13th International Conference, 2002

Little Engines of Proof.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Formal Verification of a Combination Decision Procedure.

[BibT_eX]

[DOI]

Jonathan Ford

Proceedings of the Automated Deduction, 2002

2001

Using Decision Procedures with a Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

A Technique for Invariant Generation.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Static Analysis for Safe Destructive Updates in a Functional Language.

[BibT_eX]

[DOI]

Proceedings of the Logic Based Program Synthesis and Transformation, 2001

Deconstructing Shostak.

[BibT_eX]

[DOI]

Jean-Christophe Filliâtre

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

ICS: Integrated Canonizer and Solver.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Combining Theorem Proving and Model Checking through Symbolic Analysis.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2000, 2000

Symbolic Analysis of Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the Abstract State Machines, 2000

1999

Modular Verification of SRT Division.

[BibT_eX]

[DOI]

Mandayam K. Srivas

Formal Methods Syst. Des., 1999

A case-study in component-based mechanical verification of fault-tolerant programs.

[BibT_eX]

Sandeep S. Kulkarni

Proceedings of the 1999 ICDCS Workshop on Self-stabilizing Systems, 1999

Principles and Pragmatics of Subtyping in PVS.

[BibT_eX]

[DOI]

Proceedings of the Recent Trends in Algebraic Development Techniques, 1999

Abstract and Model Check While You Prove.

[BibT_eX]

[DOI]

Hassen Saïdi

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998

Subtypes for Specifications: Predicate Subtyping in PVS.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1998

Verifying a self-stabilizing mutual exclusion algorithm.

[BibT_eX]

Shaz Qadeer

Proceedings of the Programming Concepts and Methods, 1998

Fair Synchronous Transition Systems and Their Liveness Proofs.

[BibT_eX]

[DOI]

Amir Pnueli

Eli Singerman

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998

PVS: An Experience Report.

[BibT_eX]

[DOI]

David W. J. Stringer-Calvert

Proceedings of the Applied Formal Methods, 1998

1997

Industrial Strength Formal Verification Techniques for Hardware Designs.

[BibT_eX]

[DOI]

Sreeranga P. Rajan

Mandayam K. Srivas

Proceedings of the 10th International Conference on VLSI Design (VLSI Design 1997), 1997

Integration in PVS: Tables, Types, and Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1997

Lazy Compositional Verification.

[BibT_eX]

[DOI]

Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

1996

Steps Toward Mechanizing Program Transformations Using PVS.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1996

Unifying Verification Paradigms.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1996

PVS: Combining Specification, Proof Checking, and Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Experiments in Theorem Proving and Model Checking for Protocol Verification.

[BibT_eX]

[DOI]

Klaus Havelund

Proceedings of the FME '96: Industrial Benefit and Advances in Formal Methods, 1996

PVS: Combining Specification, Proof Checking, and Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

On Shostak's Decision Procedure for Combinations of Theories.

[BibT_eX]

[DOI]

David Cyrluk

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995

Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS.

[BibT_eX]

[DOI]

Friedrich W. von Henke

IEEE Trans. Software Eng., 1995

Computer-Aided Computing.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 1995

Decision Problems for Second-Order Linear Logic

[BibT_eX]

[DOI]

Andre Scedrov

Proceedings of the Proceedings, 1995

An Integration of Model Checking with Automated Proof Checking.

[BibT_eX]

[DOI]

S. Rajan

Mandayam K. Srivas

Proceedings of the Computer Aided Verification, 1995

1994

A Tutorial on Using PVS for Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Provers in Circuit Design, 1994

Effective Theorem Proving for Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Provers in Circuit Design, 1994

Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi

[BibT_eX]

[DOI]

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Using Proof Theory to Optimize Proof Search.

[BibT_eX]

Proceedings of the ICLP 1994, 1994

Proof Search (Tutorial).

[BibT_eX]

Roy Dyckhoff

Proceedings of the ICLP 1994, 1994

Towards a Duration Calculus Proof Assistant in PVS.

[BibT_eX]

[DOI]

Jens Ulrik Skakkebæk

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

Metamathematics, machines, and Gödels's proof.

[BibT_eX]

Cambridge tracts in theoretical computer science 38, Cambridge University Press, ISBN: 978-0-521-42027-3, 1994

1993

Linearizing Intuitionistic Implication.

[BibT_eX]

[DOI]

Andre Scedrov