Recent Papers

---

• Solving Linear Arithmetic Constraints
  by Harald Rueß and Natarajan Shankar, submitted for publication, 4 Mar 2005.

• Integrating Verification Components: The Interface is the Message
  by Leonardo de Moura and Sam Owre and Harald Rue{\ss} and John Rushby and Natarajan Shankar} (to appear as book chapter)

• Justifying Equality
  by Leonardo de Moura and Harald Rueß and Natarajan Shankar, PDPAR 2004.

• An Experimental Evaluation of Ground Decision Procedures
  by Leonardo de Moura and Harald Rueß, CAV'04.

• Solving Linear Arithmetic Constraints
  by Harald Rueß and Natarajan Shankar, Technical Report, SRI International, CSL-SRI-04-01, January 2004.

• The ICS decision procedures for embedded deduction,
  by Harald Rueß and Natarajan Shankar, to be presented at CADE 2004.

• Feature-based decomposition of inductive proofs applied to real-time avionics software,
  by Vu Ha, Murali Rangarajan, Darren Cofer, Harald Rueß, and Bruno Dutertre. Accepted for publication at the 26th International Conference on Software Engineering, ICSE, May 2004.

• From Simulation to Verification (and Back)
  by Harald Rueß and Natarajan Shankar
  In: Proceedings of the 2003 Winter Simulation Conference, New Orleans, LA, December 2003, S. Chick, P.J. Sanchez, D. Ferrin, And D.J. Morrice (eds).

• The Interface is the Message
  by Harald Rueß and Natarajan Shankar
  Presented at the first QPQ Workshop on Deductive Software Components, Miami, Florid, July, 2003.

• Introducing Cyberlogic
  by Harald Rueß and Natarajan Shankar
  Presented at the third High Confidence Software and Systems Conference, Baltimore MD, April 2003.

• Embedded Deduction with ICS
  by Leonardo de Moura and Harald Rueß and John Rushby and Natarajan Shankar
  Presented at the third High Confidence Software and Systems Conference, Baltimore MD, April 2003.

• Bounded Model Checking and Induction: From Refutation to Verification
  by Leonardo de Moura, Harald Rueß, and Maria Sorea
  To be presented at CAV 200

• Monadic Second-Order Logics with Cardinalities
  by Felix Klaedtke and Harald Rueß
  In: Proceedings of 30th International Colloquium on Automata, Languages and Programming, ICALP'2003.

• Combining Shostak Theories
  by N. Shankar and Harald Rueß
  Invited paper for the Federated Logic Conference (Floc'2002) and the Conference for Rewriting Techniques and Applications (RTA'2002).

• Lazy Theorem Proving for Bounded Model Checking over Infinite Domains
  by Leonardo de Moura, Harald Rueß, and Maria Sorea
  In: Proceedings of the 18th International Conference on Automated Deduction, CADE'2002.

• Lemmas on Demand for Satisfiability Solvers
  by Leonardo de Moura, Harald Rueß
  In: Proceedings of Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT'2002. Extended version accepted for publication in the Annals of Mathematics and Artificial Intelligence (AMAI).

• Predicate Abstraction for Dense Real-Time Systems
  M. Oliver Möller, Harald Rueß, and Maria Sorea
  Electronic Notes in Theoretical Computer Science. Presented at WTPT'2002.

• Proving Secrecy is Easy Enough
  by Veronique Cortier, Jon Millen, and Harald Rueß
  In: Proceedings of the 14th Computer Security Foundations Workshop, CSFW'2001.

• Deconstructing Shostak
  by: Harald Rueß and N. Shankar
  In: Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'2001.

• Deciding Propositional Combinations of Equalities and Inequalities
  by: Jean-Christophe Filliatre, Sam Owre, Harald Rueß, and N. Shankar
  Unpublished manuscript.

• ICS: Integrated Canonizer and Solver
  by: Jean-Christophe Filliatre and Sam Owre and Harald Rueß and N. Shankar
  In: Proceedings of Computer-Aided Verification, CAV '2001.

• A Technique for Invariant Generation
  by: Ashish Tiwari, Harald Rueß, Hassen Saidi, and N. Shankar
  In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS'01.

• Rigid E-Unification Revisited
  by Ashish Tiwari, Leo Bachmair, Harald Rueß.
  In: Proceedings of Conference on Automated Deduction, CADE '2000

• Integrating WS1S with PVS
  by: Sam Owre and Harald Rueß
  Presented at CAV'00, Chicago, IL, July 2000.

• An Overview of SAL.
  Appears in the Fifth NASA Langley Formal Methods Workshop (Lfm2000).

• Protocol-Independent Secrecy
  by: Jon Millen and Harald Rueß
  Published in the proocedings of the IEEE Symposium on Security and Privacy, Oakland, CA, May, 2000.

• Polytypic Proof Construction
  by: Holger Pfeifer and Harald Rueß
  In: Proceedings of TPHOLS'99, Springer-Verlag, volume 1690 of LNCS, pp. 55--72, 1999.

• Modular Verification of SRT Division
  by: Harald Rueß, N. Shankar, M.K. Srivas
  In: Formal Methods in System Design, 14(1), pp. 45--73, Kluwer Academic Publishers, January, 1999.
  (Expanded version of conference paper.)

• Towards Light-Weight Verication and Heavy-Weight Testing (gzipped postscript)
  by: Stephan Pfab, Harald Rueß, Sam Owre, and Friedrich W. von Henke
  In: Tool Support for System Specification, Development, and Verification, R. Berghammer and Y. Lakhnech Eds., pp. 189--200, Springer Advances in Computing Science, May 1999.

• Polytypic Abstraction in Type Theory
  by: Holger Pfeifer and Harald Rueß
  Published in the Informal Proceedings of the Workshop on Generic Programming (WGP'98).

• Generic Compilation Schemes for Simple Programming Constructs
  by: Axel Dold, F.W. von Henke, Holger Pfeifer, Harald Rueß
  Technical report UIB-96-12, Universität Ulm, Fakultät für Informatik, Dec. 1996. Revised version as of January 1999.

• Guided Tour Through A Mechanized Semantics of Simple Imperative Programming Constructs
  by: Holger Pfeifer, F.W. von Henke, and Harald Rueß
  Technical Report, UIB-96-11, Universität Ulm. Revised Version as of July 1997.

• Case Studies in Meta-Level Theorem Proving
  by: F.W. von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rueß
  In: Proceedings of the 11th International Conference on Theorem Proving in Higher-Order Logics (TPHOLs '98), J. Grundy, M. Newey (Eds.), pp. 461--478, Canberra, Australia, September 1998, volume 1479 of LNCS, Springer-Verlag.

• Solving Bitvector Equations
  by: M. Oliver Möller and Harald Rueß
  In: Formal Methods in Computer-Aided Design (FMCAD'98), G. Gopalakrishnan, Ph. Windley (Eds.), pp. 36--48, Palo Alto, CA, November, 1998, volume 1522 of LNCS, Springer Verlag.

• Formal Verification of Transformations for Peephole Optimization
  by: Axel Dold, F.W. von Henke, Holger Pfeifer, and Harald Rueß
  In: Proceedings of the 4th International Symposium of Formal Methods Europe, Graz, Austria, September, 1997, Springer-Verlag.

• Hardware Verification with PVS
  by M.K. Srivas, Harald Rueß, and David Cyrluk
  in: Formal Hardware Verification: Methods and Systems in Comparison (ed. Th. Kropf), pp. 156--205 Springer-Verlag, volume 1287 of LNCS, 1997.

• An Efficient Decision Procedure for the Theory of Fixed-Sized Bitvectors
  by David Cyrluk, M. Oliver Möller, Harald Rueß
  In Orna Grumberg (Ed.), Proceedings of 9th International Conference on Computer Aided Verification, CAV'97, Haifa, Israel, June, 1997, volume 1254 of LNCS, Springer-Verlag.

• Mechanizing Domain Theory
  Falk Bartels, Holger Pfeifer, F.W. von Henke, Harald Rueß
  Technical Report UIB-96-10, Universität Ulm, 1996, Revised Version as of January 1998.

• Computation Reflection in the Calculus of Constructions and Its Application to Theorem Proving
  by Harald Rueß
  In: Proceedings of Typed Lambda Calculi and Applications (TLCA'97) P. de Groote and J.R. Hindley (Eds.), Nancy, April 1997, volume 1210 of LNCS, Springer-Verlag.

• Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study
  by Harald Rueß
  In: Proceedings of the 1st International Conference on Formal Methods in Computer-Aided Design, M. Srivas and A. Camilleri (Eds.), pp. 79--93, Palo Alto, CA, November 1996, volume 1166 of LNCS, Springer-Verlag.

• Modular Verification of SRT Division
  by Harald Rueß, N. Shankar, M.K. Srivas
  In: Proceedings of the 8th International Conference on Computer Aided Verification (CAV'96), R. Alur and Th. Henzinger (Eds.), New Brunswick, NJ, July/August 1996, volume 1102 of LNCS, Springer-Verlag.

• Reflection of Formal Tactics in a Deductive Reflection Framework
  by Harald Rueß
  In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), M.A. McRobbie and J.K. Slaney (Eds.), volume 1104 of LNAI, Springer-Verlag.

• The TYPELAB Specification and Verification Environment
  by: F.W. von Henke, Marco Luther, Holger Pfeifer, Harald Rueß, D. Schwier, and M. Strecker
  In: Proceedings of AMAST'96, M. Wirsing and M. Nivat (Eds.), pp. 604--607, volume 1101 of LNCS, Springer-Verlag.

• Construction and Deduction Methods for the Formal Development of Software
  by: F.W. von Henke, Axel Dold, Harald Rueß, and Detlef Schwier
  In KorSo: Methods , Languages, and Tools for the Construction of Correct Software, pp. 239--254, volume 1009 of LNCS, Springer-Verlag.

• Formalization and Reasoning in a Reflective Architecture
  by: Harald Rueß, Holger Pfeifer, and F.W. von Henke
  Presented at the IJCAI Workshop "Reflection and Metalevel Architectures and their Applications in AI", IJCAI'95, Montreal, Canada, July 1995.

• Towards High-Level Deductive Program Synthesis based on Type Theory
  by Harald Rueß
  In: Proceedings of the 10th Knowledge-Based Software Engineering Conference (KBSE'95), pp. 174--183, Boston, MA, November, 1995, IEEE Computer Society Press.

---

Harald Ruess: ruess@csl.sri.com