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.
-
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
(PDF) 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.
Back to SRI Formalware top level
Last modified: Tuesday 1 June 2004
by John Rushby