Dejan Jovanović and Bruno Dutertre, Interpolation and Model Checking for Nonlinear Arithmetic, to be presented at CAV 2021, JUly 2021.
Jorge A. Navas, Bruno Dutertre, and Ian A. Mason, Verification of an Optimized NTT Algorithm presented at VSTTE 2020, 12th Working Conference on Verified Software: Theories, Tools, and Experiments, July 2020.
B. Dutertre, An Empirical Evaluation of SAT Solvers on Bit-vector Problems, presented at SMT 2020 18th International Workshop on Satisfiability Modulo Theories, Paris France, July 2020. (Benchmarks).
S. Graham-Lengrand, D. Jovanović, and B. Dutertre, Solving bitvectors with MCSAT: Explanations from Bits and Pieces, International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, July 2020.
B. Dutertre, D. Jovanović, and Jorge A. Navas, Advanced Symbolic Analysis Tools for Fault-Tolerant Integrated Distributed Systems, NASA/CR-2018-21934, May 2018.
B. Dutertre, D. Jovanović, and Jorge A. Navas, Verification of Fault-Tolerant Protocols with Sally, presented at NFM 2018, Newport News, VA, April 2018. (Springer Link).
D. Jovanović and B. Dutertre, Property-Directed k-Induction, presented at FMCAD, Mountain View, CA, October 2016.
A. Tiwari, A. Gascón, and B. Dutertre, Program Synthesis Using Dual Interpretation, presented at CADE-25, Berlin, Germany. August 2015.
B. Dutertre, Solving Exists/Forall Problems With Yices, extended abstract presented at the SMT Workshop 2015, San Francisco, CA, July 2015.
A. Gascón, P. Subramanyan, B. Dutertre, A. Tiwari, D. Jovanović, S. Malik, Template-Based Circuit Understanding, presented at FMCAD, Lausanne, Switzerland, October 2014.
B. Dutertre, Yices 2.2, presented at CAV'2014, Vienna, Austria, July 2014.
A. Tiwari, B. Dutertre, D. Jovanović, T. de Candia, P. Lincoln, J. Rushby, D. Sadigh, S. Seshia, Safety Envelope for Security, presented at the 3rd International Conference on High Confidence Networked Systems, pp. 85–94, 2014.
T. King, C. Barrett, and B. Dutertre, Simplex with Sum of Infeasibilities for SMT, presented at FMCAD, Portland, OR, November 2013.
W. Steiner and B. Dutertre, The TTEthernet Synchronization Protocols and their Formal Verification, International Journal of Critical Computer-Based Systems, Vol. 4, No. 3, pp. 280–300, 2013.
B. Hall, K. Driscoll, K. Schweiker, and B. Dutertre, Investigating Actuation Force Fight with Asynchronous and Synchronous Redundancy Management Techniques, NASA/CR-2013-217984, April 2013.
B. Dutertre, A. Easwaran, B. Hall, and W. Steiner, Model-Based Analysis of Timed-Triggered Ethernet, presented at the 31st Digital Avionics Systems Conference (DASC), October 2012.
B. Dutertre, N. Shankar, and S. Owre, Integrated Formal Analysis of Timed-Triggered Ethernet, NASA/CR-2012-217554, May 2012.
B. Dutertre, Probabilistic Analysis of Distributed Fault-Tolerant Systems, NASA/CR-2011-271090, May 2011.
W. Steiner and B. Dutertre, Automated Formal Verification of the TTEthernet Synchronization Quality, presented at NASA Formal Methods (NFM 2011), Pasadena, CA, April 2011.
W. Steiner and B. Dutertre, Layered Diagnosis and Clock-Rate Correction for the TTEthernet Clock Synchronization Protocol, presented at PRDC 2011, Pasadena, CA, December 2011.
W. Steiner and B. Dutertre, SMT-Based Formal Verification of a TTEthernet Synchronization Function, presented at FMICS'2010, Antwerp, Belgium, September 2010.
N. Bjørner, B. Dutertre, and L. de Moura, Accelerating Lemma Learning Using Joins, presented at LPAR'2008, Doha, Qatar, November 2008.
L. de Moura, B. Dutertre and N. Shankar, A Tutorial on Satisfiability Modulo Theories, presented at CAV'2007, Berlin, Germany, July 2007.
B. Dutertre, Formal Modeling and Analysis of the Modbus Protocol, presented at the First Annual IFIP WG 11.10 International Conference on Critical Infrastructure Protection, Dartmouth College, NH, March 2007.
B. Dutertre and L. de Moura, A Fast Linear-Arithmetic Solver for DPLL(T), presented at CAV'2006, Seattle, Washington, August 2006.
B. Dutertre and M. Sorea, Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol using Calendar Automata, presented at FORMATS/FTRTFT'04, Grenoble, France, September 2004. Also available in PostScript.
Vu Ha, Murali Rangarajan, Darren Coffer, Harald Rueß, and Bruno Dutertre Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software, Proceedings of the 26th International Conference on Software Engineering (ICSE-2004), Edinburgh, Scotland, May 2004.
B. Dutertre, Dynamic Scan Scheduling, IEEE Real-Time Systems Symposium, pp. 327–336, Austin, TX, December 2002.
B. Dutertre, V. Crettaz, and V. Stavridou, Intrusion-Tolerant Enclaves, IEEE International Symposium on Security and Privacy, pp. 216–224, Oakland, CA, May 2002.
B. Dutertre, H. Saïdi, and V. Stavridou, Intrusion-Tolerant Group Management in Enclaves, International Conference on Dependable Systems and Networks (DSN'01), pp. 203–212, Göteborg, Sweden, July 2001.
B. Dutertre, Formal Analysis of the Priority Ceiling Protocol, IEEE Real-Time Systems Symposium (RTSS'00), pp. 151–160, Orlando, FL, November 2000.
B. Dutertre and V. Stavridou, Formal Analysis for Real-Time Scheduling, 19th AIAA/IEEE Digital Avionics Conference (DASC) , Philadelphia, PA, October 2000.
B. Dutertre, Scan Scheduling Specification and Analysis, Technical Report, System Design Laboratory, SRI International, May 2000.
B. Dutertre and V. Stavridou, Formal Requirements Analysis of an Avionics Control System, IEEE Transactions on Software Engineering, Vol. 25, No. 5, pp. 267–278, May 1997.
B. Dutertre and V. Stavridou, Requirements Analysis of Real-Time Control Systems using PVS, Lfm'97, Fourth NASA Langley Wokshop on Formal Methods, NASA Conference Publication 3356, pp. 65–73, September 1997.
B. Dutertre and S. Schneider, Using a PVS Embedding of CSP to Verify Authentication Protocols, Theorem Proving in Higher Order Logics, TPHOL's 97, LNCS 1275, pp. 121–136, August 1997.
B. Dutertre, Elements of Mathematical Analysis in PVS,Theorem Proving in Higher Order Logics, TPHOL's 96, LNCS 1125, pp. 141–156, August 1996.
B. Dutertre, Complete Proof Systems for First-Order Interval Temporal Logic, IEEE Symposium on Logic in Computer Science, LICS'95, pp. 36–43, June 1995.
B. Dutertre, Formal Modeling and Analysis of the Modbus Protocol, Technical Report, SRI International, October 2006.
B. Dutertre and L. de Moura, Integrating Simplex with DPLL(T), Technical Report SRI-CSL-06-01, May 2006.
B. Dutertre and M. Sorea, Timed Systems in SAL, Technical Report SRI-SDL-04-03, July 2004. Also available in PostScript.
B. Dutertre, S. Cheung, and J. Levy, Lightweight Key Management in Wireless Sensor Networks by Leveraging Initial Trust, Technical Report SRI-SDL-04-02, April 2004.
B. Dutertre, The Priority Ceiling Protocol: Formalization and Analysis Using PVS, Technical Report, System Design Laboratory, SRI International, October 1999.
B. Dutertre, On First Order Interval Temporal Logic, Technical Report, CSD-TR-94-3, Depatrment of Computer Science, Royal Holloway, University of London, February 1995.
B. Dutertre and S. Schneider, Embedding CSP in PVS. Applications to Authentication Protocols, Technical Report 736, Department of Computer Science, Queen Mary and Westfield College, May 1997. (Also available as Technical Report CSD-TR-97-12, Royal Holloway, University of London).
This is an expanded version of the paper above with more details on the embedding of CSP in PVS.
B. Dutertre, The Welch-Lynch Clock Synchronization Algorithm, Technical Report 747, Department of Computer Science, Queen Mary and Westfield College, March 1998.