Amir Pnueli

According to our database1, Amir Pnueli
  • authored at least 265 papers between 1969 and 2012.
  • has a "Dijkstra number"2 of three.

Awards

Turing Prize recipient

Turing Prize 1996, "For seminal work introducing temporal logic into computing science and for outstanding contributions to program and systems formal verification|verification.".

ACM Fellow

ACM Fellow 2007, "For contributions to program and system verification.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2012
Once and for all.
J. Comput. Syst. Sci., 2012

Synthesis of Reactive(1) designs.
J. Comput. Syst. Sci., 2012

Verification of multi-linked heaps.
J. Comput. Syst. Sci., 2012

Low dimensional hybrid systems - decidable, undecidable, don't know.
Inf. Comput., 2012

Effective Synthesis of Asynchronous Systems from GR(1) Specifications.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

2010
Revisiting Synthesis of GR(1) Specifications.
Proceedings of the Hardware and Software: Verification and Testing, 2010

Jtlv: A Framework for Developing Verification Algorithms.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Temporal Verification of Reactive Systems: Response.
Proceedings of the Time for Verification, 2010

Towards Component Based Design of Hybrid Systems: Safety and Stability.
Proceedings of the Time for Verification, 2010

Proving the Refuted: Symbolic Model Checkers as Proof Generators.
Proceedings of the Concurrency, 2010

2009
Synthesis of programs from temporal property specifications.
Proceedings of the 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 2009

Controller Synthesis from LSC Requirements.
Proceedings of the Fundamental Approaches to Software Engineering, 2009

2008
A Sound and Complete Deductive System for CTL* Verification.
Logic Journal of the IGPL, 2008

All You Need Is Compassion.
Proceedings of the Verification, 2008

On the Merits of Temporal Testers.
Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Program analysis for compiler validation.
Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2008

CoVaC: Compiler Validation by Program Analysis of the Cross-Product.
Proceedings of the FM 2008: Formal Methods, 2008

Discriminative Model Checking.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Checking Temporal Properties of Discrete, Timed and Continuous Behaviors.
Proceedings of the Pillars of Computer Science, 2008

Using Abstraction to Verify Arbitrary Temporal Properties.
Proceedings of the 15th Asia-Pacific Software Engineering Conference (APSEC 2008), 2008

2007
Modular Ranking Abstraction.
Int. J. Found. Comput. Sci., 2007

Specify, Compile, Run: Hardware from PSL.
Electr. Notes Theor. Comput. Sci., 2007

Shape Analysis of Single-Parent Heaps.
Proceedings of the Verification, 2007

"Don't Care" Modeling: A Logical Framework for Developing Predictive System Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Synthesizing reactive systems from LSC requirements using the play-engine.
Proceedings of the Companion to the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

Verifying Correctness of Transactional Memories.
Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Interactive presentation: Automatic hardware synthesis from specifications: a case study.
Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

On Synthesizing Controllers from Bounded-Response Properties.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
Liveness with invisible ranking.
STTT, 2006

Model Checking with Strong Fairness.
Formal Methods in System Design, 2006

Monitoring Interfaces for Faults.
Electr. Notes Theor. Comput. Sci., 2006

Reduced Functional Consistency of Uninterpreted Functions.
Electr. Notes Theor. Comput. Sci., 2006

Synthesis of Reactive(1) Designs.
Proceedings of the Verification, 2006

Ranking Abstraction of Recursive Programs.
Proceedings of the Verification, 2006

Faster Solutions of Rabin and Streett Games.
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Invisible Safety of Distributed Protocols.
Proceedings of the Automata, Languages and Programming, 33rd International Colloquium, 2006

Liveness by Invisible Invariants.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2006

From MITL to Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2006

PSL Model Checking and Run-Time Verification Via Testers.
Proceedings of the FM 2006: Formal Methods, 2006

2005
A compositional approach to CTL* verification.
Theor. Comput. Sci., 2005

A discrete-time UML semantics for concurrency and communication in safety-critical applications.
Sci. Comput. Program., 2005

Bridging the gap between fair simulation and trace inclusion.
Inf. Comput., 2005

Translation and Run-Time Validation of Loop Transformations.
Formal Methods in System Design, 2005

Validating More Loop Optimizations.
Electr. Notes Theor. Comput. Sci., 2005

Abstraction for Liveness.
Proceedings of the Verification, 2005

Shape Analysis by Predicate Abstraction.
Proceedings of the Verification, 2005

Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Temporal Logic for Scenario-Based Specifications.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Refining the Undecidability Frontier of Hybrid Automata.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

Ranking Abstraction as Companion to Predicate Abstraction.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005

Real Time Temporal Logic: Past, Present, Future.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2005

TVOC: A Translation Validator for Optimizing Compilers.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

IIV: An Invisible Invariant Verifier.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Verification of Procedural Programs.
Proceedings of the We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two, 2005

Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements.
Proceedings of the Formal Methods in Software and Systems Modeling, 2005

Ranking Abstraction as a Companion to Predicate Abstraction, .
Proceedings of the Automated Technology for Verification and Analysis, 2005

2004
Model checking and abstraction to the aid of parameterized systems (a survey).
Computer Languages, Systems & Structures, 2004

Liveness with Invisible Ranking.
Proceedings of the Verification, 2004

Deductive Verification of UML Models in TLPVS.
Proceedings of the «UML» 2004, 2004

Liveness with Incomprehensible Ranking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Smart Play-Out Extended: Time and Forbidden Elements.
Proceedings of the 4th International Conference on Quality Software (QSIC 2004), 2004

On Recognizable Timed Languages.
Proceedings of the Foundations of Software Science and Computation Structures, 2004

Range Allocation for Separation Logic.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Validating the Translation of an Industrial Optimizing Compiler.
Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003
VOC: A Methodology for the Translation Validation of OptimizingCompilers.
J. UCS, 2003

Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293).
Inf. Comput., 2003

Model-Checking and Abstraction to the Aid of Parameterized Systems.
Proceedings of the Verification, 2003

Smart play-out.
Proceedings of the Companion of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2003

Parameterized Verification by Probabilistic Abstraction.
Proceedings of the Foundations of Software Science and Computational Structures, 2003

Formal Modeling of C. elegans Development: A Scenario-Based Approach.
Proceedings of the Computational Methods in Systems Biology, First International Workshop, 2003

The ROBDD Size of Simple CNF Formulas.
Proceedings of the Correct Hardware Design and Verification Methods, 2003

Bridging the Gap between Fair Simulation and Trace Inclusion.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

TLPVS: A PVS-Based LTL Verification System.
Proceedings of the Verification: Theory and Practice, 2003

2002
Complete Proof System for QPTL.
J. Log. Comput., 2002

The Small Model Property: How Small Can It Be?
Inf. Comput., 2002

Translation and Run-Time Validation of Optimized Code.
Electr. Notes Theor. Comput. Sci., 2002

VOC: A Translation Validator for Optimizing Compilers.
Electr. Notes Theor. Comput. Sci., 2002

TimeC: A Time Constraint Language for ILP Processor Compilation.
Constraints, 2002

Automatic Verification of Probabilistic Free Choice.
Proceedings of the Verification, 2002

Applications of Formal Methods in Biology.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML.
Proceedings of the Formal Methods for Components and Objects, 2002

Smart Play-out of Behavioral Requirements.
Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Embedded Systems: Challenges in Specification and Verification.
Proceedings of the Embedded Software, Second International Conference, 2002

A Deductive Proof System for CTL.
Proceedings of the CONCUR 2002, 2002

Network Invariants in Action.
Proceedings of the CONCUR 2002, 2002

Liveness with (0, 1, infty)-Counter Abstraction.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Validating software pipelining optimizations.
Proceedings of the International Conference on Compilers, 2002

2001
Scheduling time-constrained instructions on pipelined processors.
ACM Trans. Program. Lang. Syst., 2001

Symbolic model checking with rich assertional languages.
Theor. Comput. Sci., 2001

Verification by Augmented Abstraction: The Automata-Theoretic View.
J. Comput. Syst. Sci., 2001

Automatic Deductive Verification with Invisible Invariants.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Sticks and stones: a coding scheme for parameterized verification.
Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed Computing, 2001

Range Allocation for Equivalence Logic.
Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001

From Falsification to Verification.
Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001

Beyond Regular Model Checking.
Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001

Parameterized Verification with Automatically Computed Inductive Assertions.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000
Control and Data Abstraction: The Cornerstones of Practical Formal Verification.
STTT, 2000

Propositional Temporal Logics: Decidability and Completeness.
Logic Journal of the IGPL, 2000

Verification by Augmented Finitary Abstraction.
Inf. Comput., 2000

Verification of Clocked and Hybrid Systems.
Acta Inf., 2000

A Comparison of Two Verification Methods for Speculative Instruction Execution.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

Formal Verification of the Ricart-Agrawala Algorithm.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000

Liveness and Acceleration in Parameterized Verification.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Rigorous development of embedded systems.
Proceedings of the 2000 International Conference on Compilers, 2000

1999
Decidable Integration Graphs.
Inf. Comput., 1999

Proving Refinement Using Transduction.
Distributed Computing, 1999

Verifying Tomasulo's Algoithm by Refinement.
Proceedings of the 12th International Conference on VLSI Design (VLSI Design 1999), 1999

A Framework for Scheduler Synthesis.
Proceedings of the 20th IEEE Real-Time Systems Symposium, 1999

Orthogonal Polyhedra: Representation and Computation.
Proceedings of the Hybrid Systems: Computation and Control, Second International Workshop, 1999

A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software.
Proceedings of the FM'99 - Formal Methods, 1999

Verifying Liveness by Augmented Abstraction.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999

Deciding Equality Formulas by Small Domains Instantiations.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Translation Validation: From SIGNAL to C.
Proceedings of the Correct System Design, 1999

1998
The Code Validation Tool CVT: Automatic Verification of a Compilation Process.
STTT, 1998

Translation Validation.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

Modularization and Abstraction: The Keys to Practical Formal Verification.
Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

Translation Validation for Synchronous Languages.
Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Algorithmic Verification of Linear Temporal Logic Specifications.
Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Fair Synchronous Transition Systems and Their Liveness Proofs.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998

Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Translation Validation: From DC+ to C*.
Proceedings of the Applied Formal Methods, 1998

Herbrand Automata for Hardware Verification.
Proceedings of the CONCUR '98: Concurrency Theory, 1998

On Discretization of Delays in Timed Automata and Digital Circuits.
Proceedings of the CONCUR '98: Concurrency Theory, 1998

Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk).
Proceedings of the Automated Deduction, 1998

A Fast Algorithm for Scheduling Time-Constrained Instructions on Processors with ILP.
Proceedings of the 1998 International Conference on Parallel Architectures and Compilation Techniques, 1998

1997
Verification Engineering: A Future Profession (A. M. Turing Award Lecture).
Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing, 1997

Verifying Liveness Properties of Reactive Systems (Tutorial Abstract).
Proceedings of the Hybrid and Real-Time Systems, 1997

Data-Structures for the Verification of Timed Automata.
Proceedings of the Hybrid and Real-Time Systems, 1997

Two Decades of Temporal Logic: Achievements and Challenges (Abstract).
Proceedings of the 38th Annual Symposium on Foundations of Computer Science, 1997

A Compositional Real-Time Semantics of STATEMATE Designs.
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

Verifying out-of-order executions.
Proceedings of the Advances in Hardware Design and Verification, 1997

Symbolic Model Checking with Rich ssertional Languages.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Some Progress in the Symbolic Verification of Timed Automata.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996
Verification of Clocked and Hybrid Systems.
Proceedings of the Lectures on Embedded Systems, European Educational Forum, 1996

A Platform for Combining Deductive with Algorithmic Verification.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Using Ghost Variables to Prove Refinement.
Proceedings of the Algebraic Methodology and Software Technology, 1996

1995
On the Learnability of Infinitary Regular Sets
Inf. Comput., May, 1995

Reachability Analysis of Dynamical Systems Having Piecewise-Constant Derivatives.
Theor. Comput. Sci., 1995

On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract).
STACS, 1995

Once and For All
Proceedings of the Proceedings, 1995

A Complete Proof Systems for QPTL
Proceedings of the Proceedings, 1995

Verifying Clocked Transition Systems.
Proceedings of the Hybrid Systems III: Verification and Control, 1995

Timing analysis of asynchronous circuits using timed automata.
Proceedings of the Correct Hardware Design and Verification Methods, 1995

Temporal verification of reactive systems - safety.
Springer, ISBN: 978-0-387-94459-3, 1995

1994
Temporal Proof Methodologies for Timed Transition Systems
Inf. Comput., August, 1994

Proving Partial Order Properties.
Theor. Comput. Sci., 1994

Temporal Verification Diagrams.
Proceedings of the Theoretical Aspects of Computer Software, 1994

Compositional Verification of Real-Time Systems
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Symbolic Controller Synthesis for Discrete and Timed Systems.
Proceedings of the Hybrid Systems II, 1994

Development of Hybrid Systems.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

Prooving Safety Properties of Hybrid Systems.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

1993
Probabilistic Verification
Inf. Comput., March, 1993

Models for Reactivity.
Acta Inf., 1993

Temporal Verification of Simulation and Refinement.
Proceedings of the A Decade of Concurrency, Reflections and Perspectives, 1993

In and Out of Temporal Logic
Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

Reachability Analysis of Planar Multi-limear Systems.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

A Decision Algorithm for Full Propositional Temporal Logic.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992
A Temporal Proof Methodology for Reactive Systems.
Proceedings of the Program Design Calculi, Proceedings of the NATO Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, July 28, 1992

Time for Concurrency.
Proceedings of the Future Tendencies in Computer Science, 1992

What Good Are Digital Clocks?
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

Characterization of Temporal Property Classes.
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

Verifying Hybrid Systems.
Proceedings of the Hybrid Systems, 1992

Integration Graphs: A Class of Decidable Hybrid Systems.
Proceedings of the Hybrid Systems, 1992

Towards Refining Temporal Specifications into Hybrid Systems.
Proceedings of the Hybrid Systems, 1992

Timed and Hybrid Statecharts and Their Textual Representation.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1992

System Specification and Refinement in Temporal Logic.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1992

How Vital is Liveness? Verifying Timing Properties of Reactive and Hybrid Systems (Extended Abstract).
Proceedings of the CONCUR '92, 1992

The temporal logic of reactive and concurrent systems - specification.
Springer, ISBN: 978-3-540-97664-6, 1992

1991
Completing the Temporal Picture.
Theor. Comput. Sci., 1991

What is in a Step: On the Semantics of Statecharts.
Proceedings of the Theoretical Aspects of Computer Software, 1991

From Timed to Hybrid Systems.
Proceedings of the Real-Time: Theory in Practice, 1991

Timed Transition Systems.
Proceedings of the Real-Time: Theory in Practice, 1991

Communication with Directed Logic Variables.
Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991

Temporal Proof Methodologies for Real-time Systems.
Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991

On the Faithfulness of Formal Models.
Proceedings of the Mathematical Foundations of Computer Science 1991, 1991

Specifying and Proving Serializability in Temporal Logic
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

On the Learnability of Infinitary Regular Sets.
Proceedings of the Fourth Annual Workshop on Computational Learning Theory, 1991

1990
STATEMATE: A Working Environment for the Development of Complex Reactive Systems.
IEEE Trans. Software Eng., 1990

A Hierarchy of Temporal Properties.
Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, 1990

Explicit Clock Temporal Logic
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

A temporal proof methodology for reactive systems.
Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990

An interleaving model for real-time.
Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990

Proving Partial Order Liveness Properties.
Proceedings of the Automata, Languages and Programming, 17th International Colloquium, 1990

Distributed Reactive Systems Are Hard to Synthesize
Proceedings of the 31st Annual Symposium on Foundations of Computer Science, 1990

Tight Bounds on the Complexity of Cascaded Decomposition of Automata
Proceedings of the 31st Annual Symposium on Foundations of Computer Science, 1990

1989
On the Synthesis of a Reactive Module.
Proceedings of the Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989

Specification and verification of VLSI systems.
Proceedings of the 1989 IEEE International Conference on Computer-Aided Design, 1989

On the Synthesis of an Asynchronous Reactive Module.
Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 1989

Completing the Temporal Picture.
Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 1989

Learning omega-Regular Languages from Queries and Counter-Examples (A Preliminary Report).
Proceedings of the Analogical and Inductive Inference, 1989

1988
The grammar of dimensions in machine drawings.
Computer Vision, Graphics, and Image Processing, 1988

The anchored version of the temporal framework.
Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30, 1988

STATEMATE; A Working Environment for the Development of Complex Reactive Systems.
Proceedings of the Proceedings, 1988

Applications of Temporal Logic to the Specification of Real-time Systems.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1988

A Framework for the Synthesis of Reactive Modules.
Proceedings of the Concurrency 88: International Conference on Concurrency, 1988

1987
Very High Level Concurrent Programming.
IEEE Trans. Software Eng., 1987

Specification and Verification of Concurrent Programs by forall-Automata.
Proceedings of the Temporal Logic in Specification, 1987

Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach.
Proceedings of the STACS 87, 1987

Specification and Verification of Concurrent Programs By Forall-Automata.
Proceedings of the Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, 1987

A Hierarchy of Temporal Properties (Abstract).
Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, 1987

On the Formal Semantics of Statecharts (Extended Abstract)
Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

1986
Verification of Multiprocess Probabilistic Protocols.
Distributed Computing, 1986

A Really Abstract Concurrent Model and its Temporal Logic.
Proceedings of the Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, 1986

A Choppy Logic
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Probabilistic Verification by Tableaux
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Specification and Development of Reactive Systems (Invited Paper).
IFIP Congress, 1986

Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends.
Proceedings of the Current Trends in Concurrency, Overviews and Tutorials, 1986

1985
Checking That Finite State Concurrent Programs Satisfy Their Linear Specification.
Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985

The Glory of the Past.
Proceedings of the Logics of Programs, 1985

Proving Termination of Prolog Programs.
Proceedings of the Logics of Programs, 1985

Linear and Branching Structures in the Semantics and Logics of Reactive Systems.
Proceedings of the Automata, 1985

1984
Automatic program generation in distributed cooperative computation.
IEEE Trans. Systems, Man, and Cybernetics, 1984

A Linear-History Semantics for Languages for Distributed Programming.
Theor. Comput. Sci., 1984

Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System.
Theor. Comput. Sci., 1984

Fair Termination Revisited-With Delay.
Theor. Comput. Sci., 1984

Is the Interesting Part of Process Logic Uninteresting? A Translation from PL to PDL.
SIAM J. Comput., 1984

Verification of Probabilistic Programs.
SIAM J. Comput., 1984

Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs.
Sci. Comput. Program., 1984

Now You May Compose Temporal Logic Specifications
Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30, 1984

Temporal Verification of Carrier-Sense Local Area Network Protocols.
Proceedings of the Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, 1984

Verification of Multiprocess Probabilistic Protocols.
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, 1984

A Hardware Implementation of the CSP Primitives and its Verification.
Proceedings of the Automata, 1984

On the scope of static checking in definitional languages.
Proceedings of the 1984 ACM Annual Conference on Computer Science: The fifth generation challenge, 1984

1983
Compilation of Nonprocedural Specifications into Computer Programs.
IEEE Trans. Software Eng., 1983

Termination of Probabilistic Concurrent Program.
ACM Trans. Program. Lang. Syst., 1983

Propositional Dynamic Logic of Nonregular Programs.
J. Comput. Syst. Sci., 1983

The Temporal Logic of Branching Time.
Acta Inf., 1983

On the Extremely Fair Treatment of Probabilistic Algorithms
Proceedings of the 15th Annual ACM Symposium on Theory of Computing, 1983

How to Cook a Temporal Proof System for Your Pet Language.
Proceedings of the Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, 1983

There Exit Decidable Context Free Propositional Dynamic Logics.
Proceedings of the Logics of Programs, 1983

Proving Precedence Properties: The Temporal Way.
Proceedings of the Automata, 1983

Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System (Extended Abstract).
Proceedings of the Automata, 1983

Solutions to Problem No.2.
Proceedings of the Analysis of Concurrent Systems, 1983

1982
Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness.
J. Comput. Syst. Sci., 1982

Is the Interesting Part of Process Logic Uninteresting - A Translation from PL to PDL.
Proceedings of the Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982

Termination of Probabilistic Concurrent Programs.
Proceedings of the Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982

1981
The Temporal Semantics of Concurrent Programs.
Theor. Comput. Sci., 1981

Automatic Programming of Finite State Linear Programs.
SIAM J. Comput., 1981

The Temporal Logic of Branching Time.
Proceedings of the Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, 1981

Verification of Concurrent Programs: Temporal Proof Principles.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, 1981

Further Results on Propositional Dynamic Logic of Nonregular Programs.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, 1981

Realizing an Equational Specification.
Proceedings of the Automata, 1981

Impartiality, Justice and Fairness: The Ethics of Concurrent Termination.
Proceedings of the Automata, 1981

Finite Models for Deterministic Propositional Dynamic Logic.
Proceedings of the Automata, 1981

Propositional Dynamic Logic of Context-Free Programs
Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, 1981

1980
Synchronous Schemes and Their Decision Problems.
Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980

On the Temporal Basis of Fairness.
Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980

A Linear History Semantics for Distributed Languages (Extended Abstract)
Proceedings of the 21st Annual Symposium on Foundations of Computer Science, 1980

1979
Use of a Nonprocedural Specification Language and Associated Program Generator in Software Development.
ACM Trans. Program. Lang. Syst., 1979

The Temporal Semantics of Concurrent Programs.
Proceedings of the Semantics of Concurrent Computation, 1979

The Modal Logic of Programs.
Proceedings of the Automata, 1979

1978
A Proof Method for Cyclic Programs.
Acta Inf., 1978

1977
A Direct Algorithm for Checking Equivalence of LL(k) Grammars.
Theor. Comput. Sci., 1977

Backtracking in Recursive Computations.
Acta Inf., 1977

A Complete Axiomatic System for Proving Deductions about Recursive Programs
Proceedings of the 9th Annual ACM Symposium on Theory of Computing, 1977

Simple Programs and Their Decision Problems.
Proceedings of the Automata, 1977

The Temporal Logic of Programs
Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October, 1977

1974
Axiomatic Approach to Total Correctness of Programs.
Acta Inf., 1974

1973
Decidable Properties of Monadic Functional Schemas.
J. ACM, 1973

1972
Permutation Graphs and Transitive Graphs.
J. ACM, 1972

1971
Marked Directed Graphs.
J. Comput. Syst. Sci., 1971

1970
Formalization of Properties of Functional Programs.
J. ACM, 1970

1969
Formalization of Properties of Recursively Defined Functions
Proceedings of the 1st Annual ACM Symposium on Theory of Computing, 1969


  Loading...