Specification and Verification of Controlled Systems. - Henny Sipma; Zohar Manna (FTRTFT, 1994)

Generalized Temporal Verification Diagrams. - Anca Browne; Zohar Manna; Henny Sipma (FSTTCS, 1995)

STeP: The Stanford Temporal Prover. - Zohar Manna; Nikolaj S. Bjørner; Anca Browne; Edward Y. Chang; Michael Colón; Luca de Alfaro; Harish Devarajan; Arjun Kapur; Jaejin Lee; Henny Sipma; Tomás E. Uribe (TAPSOFT, 1995)

Hierarchical Verification Using Verification Diagrams. - Anca Browne; Zohar Manna; Henny Sipma (ASIAN, 1996)

STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. - Nikolaj S. Bjørner; Anca Browne; Edward Y. Chang; Michael Colón; Arjun Kapur; Zohar Manna; Henny Sipma; Tomás E. Uribe (CAV, 1996)

Deductive Verification of Modular Systems. - Bernd Finkbeiner; Zohar Manna; Henny Sipma (COMPOS, 1997)

Abstraction and Modular Verification of Infinite-State Reactive Systems. - Zohar Manna; Michael Colón; Bernd Finkbeiner; Henny Sipma; Tomás E. Uribe (Requirements Targeting Software and Systems Engineering, 1997)

Visual Verification of Reactive Systems. - Luca de Alfaro; Zohar Manna; Henny B. Sipma; Tomás E. Uribe (TACAS, 1997)

Visual Abstractions for Temporal Verification. - Zohar Manna; Anca Browne; Henny Sipma; Tomás E. Uribe (AMAST, 1998)

Deductive Verification of Hybrid Systems Using STeP. - Zohar Manna; Henny Sipma (HSCC, 1998)

An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. - Zohar Manna; Nikolaj S. Bjørner; Anca Browne; Michael Colón; Bernd Finkbeiner; Mark C. Pichora; Henny B. Sipma; Tomás E. Uribe (Tool Support for System Specification, Development and Verification, 1998)

Verification of Parameterized Systems by Dynamic Induction on Diagrams. - Zohar Manna; Henny Sipma (CAV, 1999)

Deductive Model Checking. - Henny Sipma; Tomás E. Uribe; Zohar Manna (Formal Methods Syst. Des., 1999)

Diagram-based verification of discrete, real-time and hybrid systems. - Henny B. Sipma (1999)

Alternating the Temporal Picture for Safety. - Zohar Manna; Henny Sipma (ICALP, 2000)

Linking STeP with SPIN. - Anca Browne; Henny Sipma; Ting Zhang 001 (SPIN, 2000)

The 'Cash-Point' Service: A Verification Case Study Using STeP. - Anca Browne; Bernd Finkbeiner; Zohar Manna; Henny Sipma (Formal Aspects Comput., 2000)

Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. - Nikolaj S. Bjørner; Anca Browne; Michael Colón; Bernd Finkbeiner; Zohar Manna; Henny Sipma; Tomás E. Uribe (Formal Methods Syst. Des., 2000)

Synthesis of Linear Ranking Functions. - Michael Colón; Henny Sipma (TACAS, 2001)

Checking Finite Traces using Alternating Automata. - Bernd Finkbeiner; Henny Sipma (RV@CAV, 2001)

Deductive verification of real-time systems using STeP. - Nikolaj S. Bjørner; Zohar Manna; Henny Sipma; Tomás E. Uribe (Theor. Comput. Sci., 2001)

Delay predictive models of the National Airspace System using hybrid control theory. - Alexandre M. Bayen; Pascal Grieder; Henny Sipma; George Meyer; Claire J. Tomlin (ACC, 2002)

Practical Methods for Proving Program Termination. - Michael Colón; Henny Sipma (CAV, 2002)

Collecting Statistics over Runtime Executions. - Bernd Finkbeiner; Sriram Sankaranarayanan 001; Henny Sipma (RV@FLoC, 2002)

Petri Net Analysis Using Invariant Generation. - Sriram Sankaranarayanan 001; Henny Sipma; Zohar Manna (Verification: Theory and Practice, 2003)

Linear Invariant Generation Using Non-linear Constraint Solving. - Michael Colón; Sriram Sankaranarayanan 001; Henny Sipma (CAV, 2003)

Event Correlation: Language and Semantics. - César Sánchez 001; Sriram Sankaranarayanan 001; Henny Sipma; Ting Zhang 001; David L. Dill; Zohar Manna (EMSOFT, 2003)

Decision Procedures for Recursive Data Structures with Integer Constraints. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (IJCAR, 2004)

Non-linear loop invariant generation using Gröbner bases. - Sriram Sankaranarayanan 001; Henny Sipma; Zohar Manna (POPL, 2004)

Constraint-Based Linear-Relations Analysis. - Sriram Sankaranarayanan 001; Henny B. Sipma; Zohar Manna (SAS, 2004)

Term Algebras with Length Function and Bounded Quantifier Alternation. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (TPHOLs, 2004)

The Decidability of the First-Order Theory of Knuth-Bendix Order. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (CADE, 2005)

Final Semantics for Event-Pattern Reactive Programs. - César Sánchez 001; Henny B. Sipma; Matteo Slanina; Zohar Manna (CALCO, 2005)

Linear Ranking with Reachability. - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (CAV, 2005)

Termination Analysis of Integer Linear Loops. - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (CONCUR, 2005)

Thread Allocation Protocols for Distributed Real-Time and Embedded Systems. - César Sánchez 001; Henny B. Sipma; Venkita Subramonian; Christopher D. Gill; Zohar Manna (FORTE, 2005)

Expressive Completeness of an Event-Pattern Reactive Programming Language. - César Sánchez 001; Matteo Slanina; Henny B. Sipma; Zohar Manna (FORTE, 2005)

Decision Procedures for Queues with Integer Constraints. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (FSTTCS, 2005)

The Polyranking Principle. - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (ICALP, 2005)

LOLA: Runtime Monitoring of Synchronous Systems. - Ben D'Angelo; Sriram Sankaranarayanan 001; César Sánchez 001; Will Robinson; Bernd Finkbeiner; Henny B. Sipma; Sandeep Mehrotra; Zohar Manna (TIME, 2005)

Termination of Polynomial Programs. - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (VMCAI, 2005)

Scalable Analysis of Linear Systems Using Mathematical Programming. - Sriram Sankaranarayanan 001; Henny B. Sipma; Zohar Manna (VMCAI, 2005)

Preface. - Howard Barringer; Bernd Finkbeiner; Yuri Gurevich; Henny B. Sipma (RV@CAV, 2005)

Efficient distributed deadlock avoidance with liveness guarantees. - César Sánchez 001; Henny B. Sipma; Zohar Manna; Christopher D. Gill (EMSOFT, 2006)

Reusable models for timing and liveness analysis of middleware for distributed real-time and embedded systems. - Venkita Subramonian; Christopher D. Gill; César Sánchez 001; Henny B. Sipma (EMSOFT, 2006)

Fixed Point Iteration for Computing the Time Elapse Operator. - Sriram Sankaranarayanan 001; Henny B. Sipma; Zohar Manna (HSCC, 2006)

Proving ATL* Properties of Infinite-State Systems. - Matteo Slanina; Henny B. Sipma; Zohar Manna (ICTAC, 2006)

On efficient distributed deadlock avoidance for real-time and embedded systems. - César Sánchez 001; Henny B. Sipma; Zohar Manna; Venkita Subramonian; Christopher D. Gill (IPDPS, 2006)

Distributed Priority Inheritance for Real-Time and Embedded Systems. - César Sánchez 001; Henny B. Sipma; Christopher D. Gill; Zohar Manna (OPODIS, 2006)

What's Decidable About Arrays? - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (VMCAI, 2006)

Efficient Strongly Relational Polyhedral Analysis. - Sriram Sankaranarayanan 001; Michael Colón; Henny B. Sipma; Zohar Manna (VMCAI, 2006)

Decision procedures for term algebras with integer constraints. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (Inf. Comput., 2006)

A Family of Distributed Deadlock Avoidance Protocols and Their Reachable State Spaces. - César Sánchez 001; Henny B. Sipma; Zohar Manna (FASE, 2007)

Generating Efficient Distributed Deadlock Avoidance Controllers. - César Sánchez 001; Henny B. Sipma; Zohar Manna (IPDPS, 2007)

Verifying Balanced Trees. - Zohar Manna; Henny B. Sipma; Ting Zhang 001 (LFCS, 2007)

The Reaction Algebra: A Formal Language for Event Correlation. - César Sánchez 001; Matteo Slanina; Henny B. Sipma; Zohar Manna (Pillars of Computer Science, 2008)

Deductive verification of alternating systems. - Matteo Slanina; Henny B. Sipma; Zohar Manna (Formal Aspects Comput., 2008)

Constructing invariants for hybrid systems. - Sriram Sankaranarayanan 001; Henny B. Sipma; Zohar Manna (Formal Methods Syst. Des., 2008)