2024
Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving.
Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing, 2024
2023
Generating and Exploiting Automated Reasoning Proof Certificates.
,
,
,
,
,
,
,
,
,
,
,
,
Commun. ACM, October, 2023
Solving String Constraints Using SAT.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023
2021
Interpolation and Model Checking for Nonlinear Arithmetic.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021
2020
Solving bitvectors with MCSAT: explanations from bits and pieces (long version).
CoRR, 2020
Verification of an Optimized NTT Algorithm.
Proceedings of the Software Verification - 12th International Conference, 2020
An Empirical Evaluation of SAT Solvers on Bit-vector Problems.
Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020
Solving Bitvectors with MCSAT: Explanations from Bits and Pieces.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020
2018
Verification of Fault-Tolerant Protocols with Sally.
Proceedings of the NASA Formal Methods - 10th International Symposium, 2018
2017
LibPoly: A Library for Reasoning about Polynomials.
Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017
2016
Property-directed k-induction.
Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016
Double Helix and RAVEN: A System for Cyber Fault Tolerance and Recovery.
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the 11th Annual Cyber and Information Security Research Conference, 2016
2015
Program Synthesis Using Dual Interpretation.
Proceedings of the Automated Deduction - CADE-25, 2015
2014
Safety envelope for security.
Proceedings of the 3rd International Conference on High Confidence Networked Systems (part of CPS Week), 2014
Template-based circuit understanding.
Proceedings of the Formal Methods in Computer-Aided Design, 2014
Proceedings of the Computer Aided Verification - 26th International Conference, 2014
2013
The TTEthernet synchronisation protocols and their formal verification.
Int. J. Crit. Comput. Based Syst., 2013
Simplex with sum of infeasibilities for SMT.
Proceedings of the Formal Methods in Computer-Aided Design, 2013
2011
Layered Diagnosis and Clock-Rate Correction for the TTEthernet Clock Synchronization Protocol.
Proceedings of the 17th IEEE Pacific Rim International Symposium on Dependable Computing, 2011
Automated Formal Verification of the <i>TTEthernet</i> Synchronization Quality.
Proceedings of the NASA Formal Methods, 2011
2010
SMT-Based Formal Verification of a <i>TTEthernet</i> Synchronization Function.
Proceedings of the Formal Methods for Industrial Critical Systems, 2010
2008
Modeling and Verification of Time-Triggered Communication Protocols.
Proceedings of the 11th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2008), 2008
2007
Formal Modeling and Analysis of the Modbus Protocol.
Proceedings of the Critical Infrastructure Protection, 2007
A Tutorial on Satisfiability Modulo Theories.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007
2006
A Fast Linear-Arithmetic Solver for DPLL(T).
Proceedings of the Computer Aided Verification, 18th International Conference, 2006
Detecting Disruptive Routers in Wireless Sensor Networks.
Proceedings of the Ad-Hoc, Mobile, and Wireless Networks, 5th International Conference, 2006
2004
Using Model Checking to Assess the Dependability of Agent-Based Systems.
IEEE Intell. Syst., 2004
Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report.
Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004
Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol Using Calendar Automata.
Proceedings of the Formal Techniques, 2004
2003
Proceedings of the Security Protocols, 2003
Dependable Intrusion Tolerance: Technology Demo.
Proceedings of the 3rd DARPA Information Survivability Conference and Exposition (DISCEX-III 2003), 2003
Self-regenerative software components.
Proceedings of the 2003 ACM Workshop on Survivable and Self-Regenerative Systems, 2003
Forum Session: Security for Wireless Sensor Networks.
Proceedings of the 19th Annual Computer Security Applications Conference (ACSAC 2003), 2003
2002
An Architecture for an Adaptive Intrusion-Tolerant Server.
Proceedings of the Security Protocols, 2002
Intrusion-Tolerant Enclaves.
Proceedings of the 2002 IEEE Symposium on Security and Privacy, 2002
Proceedings of the 23rd IEEE Real-Time Systems Symposium (RTSS'02), 2002
2001
Intrusion-Tolerant Group Management in Enclaves.
Proceedings of the 2001 International Conference on Dependable Systems and Networks (DSN 2001) (formerly: FTCS), 2001
2000
Formal Analysis of the Priority Ceiling Protocol.
Proceedings of the 21st IEEE Real-Time Systems Symposium (RTSS 2000), 2000
1999
A Formalization of Software Architecture.
Proceedings of the FM'99 - Formal Methods, 1999
1997
Formal Requirements Analysis of an Avionics Control System.
IEEE Trans. Software Eng., 1997
Using a PVS Embedding of CSP to Verify Authentication Protocols.
Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997
1996
Elements of Mathematical Analysis in PVS.
Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996
1995
The practice of formal methods in safety-critical systems.
J. Syst. Softw., 1995
Complete Proof Systems for First Order Interval Temporal Logic
Proceedings of the Proceedings, 1995