Recent Papers on Formal Methods from SRI

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Here's some troubleshooting help if the files don't display properly.

More papers can be found by by following links to our personal home pages.

2004

• Generating Efficient Test Sets with a Model Checker by Grégoire Hamon, Leonardo de Moura, and John Rushby. Presented at SEFM '04, Beijing, China, September 2004; appears in the proceedings published by IEEE, pp. 261-270.
• Modeling and Verification of a Fault-Tolerant Real-time Startup Protocol using Calendar Automata by Bruno Dutertre (SRI SDL) and Maria Sorea. Presented at FTRTFT '04, Grenoble, France, September 2004. Appears in Springer Verlag LNCS 3253, pp. 199-214.
• Termination of linear programs by Ashish Tiwari. Presented at CAV 2004, Boston, MA, July 2004. Appears in Springer Verlag LNCS 3114, pp. 70-82.
• An Experimental Evaluation of Ground Decision Procedures by Leonardo de Moura, and Harald Rueß. Presented at CAV 2004, Boston, MA, July 2004. Appears in Springer Verlag LNCS 3114, pp. 162-174.
• SAL 2 by Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, N. Shankar, Maria Sorea, and Ashish Tiwari. Presented at CAV 2004, Boston, MA, July 2004. Appears in Springer Verlag LNCS 3114, pp. 496-500.
• The ICS Decision Procedures for Embedded Deduction by Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, and N. Shankar. Presented at IJCAR 2004, Cork, Ireland, July 2004. Appears in Springer Verlag LNCS 3097, pp. 218-222.
• Justifying Equality by Leonardo de Moura, Harald Rueß and Natarajan Shankar. Presented at PDPAR 2004, Cork, Ireland, July 2004
• Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation by Wilfried Steiner, John Rushby, Maria Sorea, and Holger Pfeifer. Presented at DSN '04, Florence, Italy, June 2004; appears in the proceedings published by IEEE, pp. 189-198.
• Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software by Vu Ha (Honeywell), Murali Rangarajan (Honeywell), Darren Cofer (Honeywell), Harald Rueß and Bruno Dutertre. Presented at 26th International Conference on Software Engineering (ICSE-2004), Edinburgh, Scotland, May 2004; appears in the proceedings published by IEEE, pp. 304-313.
• Symbolic systems biology: Hybrid modeling and analysis of biological networks by Pat Lincoln and Ashish Tiwari. Presented at HSCC 2004, Univ. of Pennsylvania, Philadelphia, March 2004. Appears in Springer Verlag LNCS 2993, pp. 660-672.
• Nonlinear Systems: Approximating Reach Sets by Ashish Tiwari and Gaurav Khanna. Presented at HSCC 2004, Univ. of Pennsylvania, Philadelphia, March 25-27 2004. Appears in Springer Verlag LNCS 2993, pp. 600-614,
• An Operational Semantics for Stateflow by Grégoire Hamon and John Rushby. Presented at FASE '04, Barcelona, Spain, March 2004. Appears in Springer Verlag LNCS 2984, pp. 229-243.

2003

• Invisible Formal Methods for Embedded Control Systems by Ashish Tiwari, John Rushby, and Natarajan Shankar. Proceedings of the IEEE, 91(1): 29-39, January 2003.