Selected Publications of the
STeP research group
(View by topic)
2006
 Cesar Sanchez, Henny B. Sipma, Christopher D. Gill, and Zohar
Manna, Distributed Priority Inheritance
for RealTime and
Embedded Systems. To appear in OPODIS'06.
 Matteo Slanina, Henny B. Sipma, and Zohar Manna,
Proving ATL* Properties of InfiniteState
Systems. To appear in ICTAC'06.
 Venkita Subramonian, Christopher Gill, Cesar Sanchez, and Henny B.
Sipma, Reusable Models for Timing and Liveness Analysis of Middleware
for Distributed RealTime and Embedded Systems. To appear in EMSOFT'06.
 Cesar Sanchez, Henny B. Sipma, Zohar Manna, Christopher D. Gill,
Efficient Distributed Deadlock Avoidance
with Liveness Guarantees. To appear in EMSOFT'06.
 Ting Zhang, Henny B. Sipma, Zohar Manna,
Decision procedures for term algebras with integer
constraints, In Information and Computation, volume 204,
pp 15261574, October 2006.
 Cesar Sanchez, Henny B. Sipma, Zohar Manna, Venkita Subramonian,
and Christopher D. Gill, On Efficient
Distributed Deadlock Avoidance
for Distributed RealTime and Embedded Systems, In Proc. of the
20th IEEE Int'l Parallel and Distributed Processing Symposium
(IPDPS'06), IEEE Computer Society Press, 2006.
 Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna,
Fixed point
iteration for computing the time elapse operator, In Proc. Hybrid
Systems: Computation and Control (HSCC 2006), Lecture Notes in
Computer Science. Vol. 3927, Springer Verlag, 2006.
 Aaron R. Bradley, Zohar Manna, Henny B. Sipma,
What's decidable about Arrays?,
In Proc. Verification, Model Checking,
and Abstract Interpretation (VMCAI 2006), Lecture Notes in Computer
Science, Vol. 3855, Springer Verlag, 2006.
 Sriram Sankaranarayanan, Michael A. Colon, Henny B. Sipma, Zohar
Manna,
Efficient Strongly Relational Polyhedral
Analysis, In Proc.
Verification, Model Checking,
and Abstract Interpretation (VMCAI 2006), Lecture Notes in Computer
Science, Vol. 3855, Springer Verlag, 2006.
2005
 Ting Zhang, Henny B. Sipma, Zohar Manna,
Decision Procedures for Queues with Integer
Constraints, In Proc. Foundations of Software Technology and
Theoretical Computer Science (FSTTCS), December 2005,
Lecture Notes in Computer Science, Volume 3821, SpringerVerlag.
 Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny B. Sipma,
Collecting statistics about runtime executions. In
Formal Methods in System Design, Vol. 27, pp 253274.
 Cesar Sanchez, Henny B. Sipma, Venkita Subramonian,
Christopher Gill, Zohar Manna,
Thread Allocation Protocols
for Distributed RealTime and Embedded Systems. In Formal
Techniques for Networked and Distributed Systems (FORTE 2005):
25th IFIP WG 6.1 International Conference, October 2005,
Lecture Notes in Computer Science, Volume 3731, Springer Verlag,
pp 159173.
 Cesar Sanchez, Matteo Slanina, Henny B. Sipma, Zohar Manna,
Expressive Completeness of an
EventPattern Reactive Programming Language. In Formal
Techniques for Networked and Distributed Systems (FORTE 2005):
25th IFIP WG 6.1 International Conference, October 2005,
Lecture Notes in Computer Science, Volume 3731, Springer Verlag,
pp 529532.
 Sriram Sankaranarayanan,
Mathematical Analysis of Programs,
PhD Thesis, Stanford University.
 Aaron R. Bradley, Zohar Manna, Henny B. Sipma,
Termination Analysis of Integer Linear Loops,
In Proc. of the 16th International Conference on
Concurrency Theory (CONCUR'05), San Francisco, August 2005,
Springer Verlag, LNCS 3653, pp 488502.
 Ting Zhang, Henny B. Sipma, Zohar Manna,
The Decidability of the Firstorder Theory of KnuthBendix Order,
In Proc. of the 20th International Conference on
Automated Deduction (CADE'05), Tallinn, Estonia, July 2005,
Springer Verlag, LNCS 3632, pp 131148.
 Cesar Sanchez, Henny B. Sipma, Matteo Slanina, Zohar Manna,
Final Semantics for EventPattern Reactive
Programs, In Proc. of the First Conference on Algebra and Coalgebra
in Computer Science (CALCO'05), Swansea, UK, September 2005,
Springer Verlag, LNCS 3629, pp 364378.
 Aaron R. Bradley, Zohar Manna, Henny B. Sipma,
Linear Ranking with Reachability,
In Proc. of 17th International Conference on
Computer Aided Verification (CAV'05), Springer Verlag, 2005,
LNCS 3576, pp 491504.
 Aaron R. Bradley, Zohar Manna, Henny B. Sipma,
The Polyranking Principle,
In Proc. 32nd International Colloquium on Automata,
Languages and Programming (ICALP 2005), Lisboa, Portugal, July 2005,
Springer Verlag, LNCS 3580, pp 13491361.
 Ben d'Angelo, Sriram Sankaranarayanan, Cesar Sanchez, Will
Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra,
Zohar Manna, LOLA: Runtime Monitoring of
Synchronous Systems,
In Proc. of the 12th International Symposium of Temporal Representation
and Reasoning (TIME 2005), pp. 166174, IEEE Computer Society Press,
2005.
 Aaron R. Bradley, Zohar Manna, Henny B. Sipma,
Termination of Polynomial Programs,
In Proc. of Verification, Model Checking and Abstract
Interpretation (VMCAI'05), LNCS 3385, Springer Verlag, 2005.
 Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna,
Scalable Analysis of Linear Systems using
Mathematical Programming, In
Proc.of Verification, Model Checking and Abstract
Interpretation (VMCAI'05), LNCS 3385, pp 2147, Springer Verlag, 2005.
2004
 Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna,
ConstraintBased LinearRelations Analysis, In
Static Analysis Symposium (SAS'04), LNCS 3148 Springer Verlag,
pp 5368 .
 Ting Zhang, Henny B. Sipma, and Zohar Manna,
Term algebras with
length function and bounded quantifier alternation. In
17th Internation Conference on Theorem Proving in Higher Order
Logics (TPHOLS'04), LNCS 3223, pp 321336, Springer Verlag 2004.
 Ting Zhang, Henny B. Sipma, and Zohar Manna,
Decision procedures
for recursive data structures with integer constraints. In
International Joint Conference on Automated Reasoning (IJCAR'04),
LNCS 3097, Springer Verlag, pp 152167, 2004.
 Calogero G. Zarba, The Combination Problem in Automated Reasoning.
PhD thesis, Stanford University, 2004.
 Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna,
Constructing Invariants for Hybrid systems.
In Hybrid Systems: Computation and Control (HSCC 2004).
 Bernd Finkbeiner and Henny B. Sipma, Checking Finite Traces Using
Alternating Automata. In Formal Methods in System Design, vol 24,
pages 101127.
 Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna,
NonLinear Loop Invariant Generation,
In Principles of Programming
Languages (POPL 2004).
 Sriram Sankaranarayanan, Henny Sipma, Zohar Manna,
Petri Net
Analysis Using Invariant Generation. In Verification:
Theory and Practice, vol.
2772 of Lecture Notes in Computer Science, 2004.
 Calogero Zarba,
Combining
Sets with Elements, In Verification:
Theory and Practice, vol.
2772 of Lecture Notes in Computer Science, 2004.
2003
 Zohar Manna and Calogero Zarba,
Combining decision procedures. In Formal Methods at the
Crossroads: from Panacea to Foundational Support,
Vol 2787 of Lecture Notes in Computer Science, pp 381422.
 Cesar Sanchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang,
David Dill, and Zohar Manna,
Event Correlation: Language and Semantics,
In Embedded Software (EMSOFT), vol 2855 of Lecture Notes in
Computer Science, Springer Verlag, pp 323339.
 Calogero G. Zarba, Zohar Manna, Henny Sipma,
Combining Theories
Sharing Dense Orders. In Automated Reasoning with Analytic Tableaux
and Related Methods:
Position Papers and Tutorials
Marta Cialdea Mayer and Fiora Pirri, editors. Technical Report
RTDIA802003, pages 8398, Universitą di Roma Tre. Aracne Editrice, 2003
 Michael A. Colon, Deductive Techniques for Program Analysis,
PhD Thesis, Stanford University.
 Michael A. Colon, Sriram Sankaranarayanan, Henny B. Sipma.
Linear
Invariant Generation using Nonlinear Constraint Solving. In
Computer Aided
Verification (CAV 2003), vol. 2725 of Lecture Notes in Computer
Science, Springer Verlag, pp. 420433.
 Henny Sipma. A Formal Model for CrossCutting Modular Transition Systems,
Workshop on Foundations of AspectOriented Languages (FOAL 2003), Boston,
March 2003.
2002
 Bernd Finkbeiner, Verification Algorithms based on Alternating
Automata, PhD Thesis, Stanford University.
 Bernd Finkbeiner, Sriram Sankaranarayanan and Henny Sipma.
Collecting Statistics over Runtime Executions.
In RV'02.
 Michael Colon and Henny Sipma.
Practical Methods for Proving Program Termination.
In 14th International Conference on Computer Aided Verification (CAV),
LNCS 2404, SpringerVerlag, pp 442454, 2002.
 Alexandre M. Bayen, Pascal Grieder, Henny Sipma, George Meyer, and
Claire J. Tomlin, Delay Predictive Models of the National Airspace
System Using Hybrid Control Theory. In American Control Conference,
WM pp 767772.
 Calogero G. Zarba.
A tableau calculus for combining nondisjoint
theories. To appear in TABLEAUX'02.
 Calogero G. Zarba. Combining Multisets with
Integers. To appear
in CADE'02.
 Calogero G. Zarba. Combining Sets with Integers,
In Alessandro Armando, editor, Frontiers of Combining Systems (FROCOS 2002),
Lecture Notes in Artificial Intelligence, Springer Verlag, 2002.
 Matteo Slanina. Control Rules for Reactive
System Games. 2002 AAAI Spring Symposium on LogicBased
Program Synthesis.
2001
 Calogero G. Zarba. Combining NonDisjoint
Theories. In Rajeev Gorč,
Alexander Leitsch, and Tobias Nipkow, editors, International Joint
Conference on Automated Reasoning. Short Papers (IJCAR 2001),
Technical Report DII 11/01, pages 180189. University of Siena, Italy,
2001.
 Calogero G. Zarba. Combining Lists with Integers
. In Rajeev Gorč,
Alexander Leitsch, and Tobias Nipkow, editors, International Joint
Conference on Automated Reasoning. Short Papers (IJCAR 2001),
Technical Report DII 11/01, pages 170179. University of Siena, Italy, 2001.
 Bernd Finkbeiner and Henny Sipma. Checking Finite Traces using Alternating Automata.
Workshop on Runtime Verification, CAV'01, 2001.
 Nikolaj Bjorner, Zohar Manna, Henny Sipma and Tomás
Uribe. Deductive
Verification of Realtime Systems using STeP.
Theoretical Computer Science, (253) 2001, pp 2760.
 Michael Colon, Henny Sipma.
Synthesis of Linear Ranking Functions.
In 7th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS),
LNCS 2031, SpringerVerlag, pp 6781.
 Bernd Finkbeiner. Language Containment
Checking with Nondeterministic
BDD's. In 7th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS),
LNCS 2031, SpringerVerlag, pp 2438.
 Henny Sipma, Tomas Uribe, and Zohar Manna.
Model checking and deduction for infinitestate systems
. In Logical Perspectives on Language and Information, pp 221244,
CSLI publications, 2001.
2000
 Zohar Manna, Henny Sipma,
Verification Diagrams: Logic + Automata, In Proceedings
of the7th Monterey Workshop: Modelling Software Systems
Structures in a Fastly Moving Scenario, pp 226237,
Santa Margherita, 2000.
 Zohar Manna, Henny Sipma,
Alternating the Temporal Picture for Safety.
In Proc. 27th Intl. Colloq. Aut. Lang. Prog.(ICALP).
LNCS 1853, SpringerVerlag, pp 429450.
 Anca Browne, Henny Sipma, Ting Zhang.
Linking STeP with SPIN.
In 7th International SPIN Workshop: SPIN Model Checking and
Software Verification, LNCS 1885, SpringerVerlag, pp 181186.
 Anca Browne, Bernd Finkbeiner, Zohar Manna, Henny Sipma,
The `CashPoint' Service: A Verification Case Study Using STeP.
Formal Aspects of Computing 12 (2000) 4, 218219
 Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd Finkbeiner,
Zohar Manna, Henny Sipma, Tomas Uribe.
Verifying Temporal Properties
of Reactive Systems: A STeP Tutorial. In Formal Methods in
System Design, vol 16, pp 227270.
1999
 Zohar Manna and Henny Sipma,
Verification of Parameterized
Systems by Dynamic Induction on Diagrams,
CAV'99, pp 2543, LNCS 1633, SpringerVerlag, 1999.
 Henny B. Sipma, Tomás E. Uribe and Zohar Manna.
Deductive Model Checking.
Formal Methods in System Design, Vol 15, pp 4974
(1999).
 Zohar Manna, Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd
Finkbeiner, Mark Pichora, Henny B. Sipma, Tomas Uribe.
An Update on STeP: DeductiveAlgorithmic Verification of Reactive
Systems. In Tool Support for System Specification, Development
and Verification, Advances in Computing Science,
pp 174188, Springer Verlag, 1999.
 Henny Sipma.
Diagrambased verification of reactive,
realtime, and hybrid systems. PhD Thesis.
1998
 Zohar Manna and Henny Sipma.
Deductive Verification of Hybrid
Systems using STeP. In Hybrid Systems: Computation and
Control, Lecture Notes in Computer Science 1386,
SpringerVerlag, 1998.
 Bernd Finkbeiner, Zohar Manna and Henny Sipma.
Deductive
Verification of Modular Systems. Compositionality: The
Significant Difference, COMPOS'97, LNCS vol. 1536, pp 239275,
1998.
 Zohar Manna, Anca Browne, Henny Sipma, and Tomas Uribe.
Visual
Abstraction for Temporal Verification. In AMAST'98,
Vol 1548 of LNCS, pp 2841, SpringerVerlag, 1998.
 Michael Colon and Tomas Uribe,
Generating FiniteState Abstractions
of Reactive Systems Using Decision Procedures. In International
Conference on ComputerAided Verification, CAV'98, pp. 293304,
vol. 1427 of LNCS, SpringerVerlag, June/July 1998.
 Zohar Manna, Michael Colon, Bernd Finkbeiner, Henny Sipma, and
Tomas Uribe.
Abstraction and Modular Verification of InfiniteState
Reactive Systems.
Requirements Targeting Software and Systems
Engineering (RTSE), LNCS 1526, Springer Verlag, pp 273292, 1998.
 Luca de Alfaro, Zohar Manna and Henny B. Sipma.
Decomposing,
Transforming and Composing Diagrams: The joys of Modular
Verification,
Technical Report STANCS981614, Stanford University, 1998.
 Nikolaj Bjorner.
Integrating Decision Procedures for Temporal
Verification. PhD Thesis, Stanford University.
 Tomas Uribe.
Abstractionbased DeductiveAlgorithmic Verification
of Reactive Systems. PhD Thesis. Appeared as
Technical Report STANCSTR991618, Stanford University.
1997

Nikolaj Bjørner, I. Anca Browne and Zohar Manna.
Automatic Generation of
Invariants and Intermediate Assertions.
Theoretical Computer Science, vol. 173(1), pp. 4987,
February 1997.
Original version appeared in
1st International Conference on Principles and Practice of
Constraint Programming, Lecture Notes in Computer Science 976,
Cassis, France, pp. 589623,
September 1995.
 Arjun Kapur, Interval and Pointbased Approaches to Hybrid Systems
Verification,
PhD Thesis, Stanford University, August 1997.
 Nikolaj Bjørner, Uri Lerner, and Zohar Manna.
Deductive Verification of Parameterized FaultTolerant Systems:
A Case Study.
In Proc. of International Conference on Temporal Logic, Kluwer, July 1997.
 Luca de Alfaro, Arjun Kapur and Zohar Manna.
Hybrid Diagrams: A
DeductiveAlgorithmic Approach to Hybrid System Verification.
In Proc. of 14th Symposium on Theoretical Aspects of Computer Science,
vol. 1200 of Lecture Notes in Computer Science, pp. 153164,
Springer Verlag, Feb. 1997.
 Luca de Alfaro, Zohar Manna, Henny B. Sipma and
Tomás E. Uribe.
Visual Verification of Reactive Systems,
in Third International Workshop on Tools and Algorithms for the
Construction and Analysis of Systems, Lecture Notes in Computer
Science, SpringerVerlag, 1997.
 Nikolaj Bjørner, Zohar Manna, Henny Sipma and Tomás
Uribe.
Deductive Verification of Realtime Systems using STeP,
4th International AMAST Workshop on Realtime Systems,
LNCS vol 1231, SpringerVerlag, pp 2243, 1997.
 Henny B. Sipma, Tomás E. Uribe and Zohar Manna.
Model
Checking and Deduction for Verifying Infinitestate
Systems. Logic, Language and Computation, CSLI, 1997.
 Nikolaj Bjørner, Mark Stickel and Tomás E. Uribe.
A Practical Integration of FirstOrder
Reasoning and Decision Procedures, Proceedings of the 14th
Intl. Conf. on Automated Deduction, LNCS vol 1249,
SpringerVerlag, pp 101115, 1997.
1996
 Henny B. Sipma, Tomás E. Uribe and Zohar Manna.
Deductive Model Checking.
In 8th International Conference on ComputerAided Verification,
LNCS vol. 1102, pp. 209219, SpringerVerlag, July 1996.
 Luca de Alfaro and Zohar Manna.
Temporal Verification by Diagram Transformations.
In 8th International Conference on ComputerAided Verification,
LNCS vol. 1102, pp. 287299, SpringerVerlag, July 1996.
 Nikolaj Bjorner, Anca Browne, Eddie Chang, Michael Colon,
Arjun Kapur, Zohar Manna, Henny Sipma, Tomas Uribe,
STeP: DeductiveAlgorithmic Verification
of Reactive and Realtime Systems,
In 8th International Conference on ComputerAided Verification,
LNCS vol. 1102, pp. 415418, SpringerVerlag, July 1996.
 Anca Browne, Luca de Alfaro, Zohar Manna, Henny B. Sipma
and Tomás E. Uribe.
DiagramBased Formalisms for the Verification of Reactive Systems,
in CADE13 Workshop on Visual Reasoning, New Brunswick, NJ, July 1996.
1995
 Nikolaj Bjorner, Anca Browne, Eddie Chang, Michael Colon,
Arjun Kapur, Zohar Manna, Henny Sipma, Tomas Uribe,
STeP: The Stanford Temporal Prover (Educational Release), User's Manual.
Technical report STANCSTR951562, Computer Science Department,
Stanford University, November 1995.
 Anuchit Anuchitanukul, Synthesis of Reactive Programs, PhD Thesis,
Stanford University, September 1995.
 Zohar Manna and Henny Sipma.
A Deductive Approach towards Controller Synthesis. In 1995 IEEE
International Symposium on Intelligent Control, Monterey, CA,
1995, pp. 3541.
 Anuchit Anuchitanukul, Zohar Manna and Tomás E. Uribe.
Differential BDDs.
In J. van Leeuwen, ed, Computer Science Today ,
Lecture Notes in Computer Science, Vol. 1000, pp. 218233,
SpringerVerlag, Sep. 1995.
 I. Anca Browne, Zohar Manna and Henny Sipma.
Generalized Temporal Verification
Diagrams. In 15th Conference on the Foundations of Software
Technology and Theoretical Computer Science,
Lecture Notes in Computer Science, Bangalore, India (December 1995).

The STeP group.
STeP:
The Stanford Temporal Prover (2page abstract).
In TAPSOFT'95: Theory and Practice of Software Development,
Lecture Notes in Computer Science 915, May 1995, pp. 793794.
 Luca de Alfaro and Zohar Manna,
Verification in Continuous Time by Discrete Reasoning,
4th International Conference on
Algebraic Methodology and Software Technology (AMAST), Montreal,
Canada, pp. 292306, July 1995.
1994

Zohar Manna, Anuchit Anuchitanukul, Nikolaj Bjorner, Anca Browne,
Edward Chang, Michael Colon, Luca de Alfaro, Harish Devarajan,
Henny Sipma and Tomas Uribe,
STeP: The Stanford Temporal Prover.
Technical report STANCSTR941518, Computer Science Department,
Stanford University, July 1994.
 Anuchit Anuchitanukul and Zohar Manna, Realizability and Synthesis
of Reactive Modules, In Computer Aided Verification (CAV'94), LNCS 818,
Springer Verlag, pp 156169, 1994.
 Henny Sipma and Zohar Manna.
Specification and Verification of Controlled
Systems. In
Proceedings of the Third International Symposium on Formal
Techniques in RealTime and FaultTolerant Systems, Lecture notes
in Computer Science 863, SpringerVerlag, 1994.
 Arjun Kapur, Thomas A. Henzinger, Zohar Manna and Amir Pnueli.
Proving Safety Properties of Hybrid Systems.
International Symposium on Formal Techniques in Real Time and
Fault Tolerant Systems, Lecture Notes in Computer Science 863,
pp. 431454, SpringerVerlag, 1994.
 Edward Chang, Zohar Manna and Amir Pnueli.
Compositional Verification of Realtime Systems.
In IEEE Symposium on Logic in Computer Science,
pp. 458465, Paris, 1994.
Last modified: Mon Feb 4 15:01:33 PST 2002