Rajeev Alur

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Can we verify cyber-physical systems?: technical perspective.

[BibT_eX]

[DOI]

Commun. ACM, 2013

TRANSIT: specifying protocols with concolic snippets.

[BibT_eX]

[DOI]

Abhishek Udupa

Arun Raghavan

Sela Mador-Haim

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Tutorial I: Syntax-guided synthesis.

[BibT_eX]

[DOI]

Proceedings of the 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2013

From Monadic Second-Order Definable String Transformations to Transducers.

[BibT_eX]

[DOI]

Antoine Durand-Gasselin

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Regular Functions and Cost Register Automata.

[BibT_eX]

[DOI]

Loris D'Antoni

Mukund Raghothaman

Yifei Yuan

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

On the Complexity of Shortest Path Problems on Discounted Cost Graphs.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2013

Automated Grading of DFA Constructions.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2013, 2013

Decision Problems for Additive Regular Functions.

[BibT_eX]

[DOI]

Mukund Raghothaman

Proceedings of the Automata, Languages, and Programming - 40th International Colloquium, 2013

Safe schedulability of bounded-rate multi-mode systems.

[BibT_eX]

[DOI]

Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Towards synthesis of platform-aware attack-resilient control systems: extended abstract.

[BibT_eX]

[DOI]

Proceedings of the 2nd ACM International Conference on High Confidence Networked Systems (part of CPS Week), 2013

Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels.

[BibT_eX]

[DOI]

Jay Thakkar

Aditya Kanade

Proceedings of the Formal Techniques for Distributed Systems, 2013

On the feasibility of automation for bandwidth allocation problems in data centers.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Counter-strategy guided refinement of GR(1) temporal logic specifications.

[BibT_eX]

[DOI]

Salar Moarref

Ufuk Topcu

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Syntax-guided synthesis.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Algorithmic analysis of array-accessing programs.

[BibT_eX]

[DOI]

Scott Weinstein

ACM Trans. Comput. Log., 2012

Time-Triggered Implementations of Dynamic Controllers.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2012

2011 CAV award announcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2012

2010 CAV award announcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2012

Modeling and Verification of a Dual Chamber Implantable Pacemaker.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Regular Transformations of Infinite Strings.

[BibT_eX]

[DOI]

Emmanuel Filiot

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Optimal scheduling for constant-rate multi-mode systems.

[BibT_eX]

[DOI]

Dominik Wojtczak

Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

An Axiomatic Memory Model for POWER Multiprocessors.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Software model checking using languages of nested trees.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2011

Compositional Modeling and Analysis of Multi-Hop Control Networks.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2011

Regular Functions, Cost Register Automata, and Generalized Min-Cost Problems

[BibT_eX]

[DOI]

Loris D'Antoni

Mukund Raghothaman

Yifei Yuan

CoRR, 2011

Streaming String Transducers.

[BibT_eX]

[DOI]

Proceedings of the Logic, Language, Information and Computation, 2011

Streaming transducers for algorithmic verification of single-pass list-processing programs.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Nondeterministic Streaming String Transducers.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming - 38th International Colloquium, 2011

Interfaces for Control Components.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2011

Relating average and discounted costs for quantitative analysis of timed systems.

[BibT_eX]

[DOI]

Proceedings of the 11th International Conference on Embedded Software, 2011

Formal verification of hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the 11th International Conference on Embedded Software, 2011

Litmus tests for comparing memory consistency models: how long do they need to be?

[BibT_eX]

[DOI]

Sela Mador-Haim

Proceedings of the 48th Design Automation Conference, 2011

2010

Active Learning of Plans for Safety and Reachability Goals With Partial Observability.

[BibT_eX]

[DOI]

IEEE Trans. Syst. Man Cybern. Part B, 2010

Algorithmic Verification of Single-Pass List Processing Programs

[BibT_eX]

[DOI]

CoRR, 2010

Temporal Reasoning for Procedural Programs.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Representation dependence testing using program inversion.

[BibT_eX]

[DOI]

Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Expressiveness of streaming string transducers.

[BibT_eX]

[DOI]

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010

Generating Litmus Tests for Contrasting Memory Consistency Models.

[BibT_eX]

[DOI]

Sela Mador-Haim

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Model Checking of Linearizability of Concurrent List Implementations.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Adding nesting structure to words.

[BibT_eX]

[DOI]

J. ACM, 2009

Modeling and Analysis of Multi-hop Control Networks.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE Real-Time and Embedded Technology and Applications Symposium, 2009

Specification and Analysis of Network Resource Requirements of Control Systems.

[BibT_eX]

[DOI]

Sebastian Fischmeister

Madhukar Anand

Proceedings of the Hybrid Systems: Computation and Control, 12th International Conference, 2009

On Omega-Languages Defined by Mean-Payoff Conditions.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2009

Temporal Reasoning about Program Executions.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2009

Robust stability of multi-hop control networks.

[BibT_eX]

[DOI]

Proceedings of the 48th IEEE Conference on Decision and Control, 2009

Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models.

[BibT_eX]

[DOI]

Sriram Sankaranarayanan

K. C. Shashidhar

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Automated Analysis of Java Methods for Confidentiality.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Scalable scheduling algorithms for wireless networked control systems.

[BibT_eX]

[DOI]

Alf J. Isaksson

Proceedings of the IEEE Conference on Automation Science and Engineering, 2009

2008

First-Order and Temporal Logics for Nested Words.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2008

Automatic symbolic compositional verification by learning assumptions.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2008

Introduction.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2008

Model Checking: From Tools to Theory.

[BibT_eX]

[DOI]

Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Regular Specifications of Resource Requirements for Embedded Control Software.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE Real-Time and Embedded Technology and Applications Symposium, 2008

RTComposer: a framework for real-time components with scheduling interfaces.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM & IEEE International conference on Embedded software, 2008

Symbolic analysis for improving simulation coverage of Simulink/Stateflow models.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM & IEEE International conference on Embedded software, 2008

Ranking Automata and Games for Prioritized Requirements.

[BibT_eX]

[DOI]

Aditya Kanade

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Marrying Words and Trees.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Methodology and Software Technology, 2008

2007

Dispatch sequences for embedded control models.

[BibT_eX]

[DOI]

Arun Chandrashekharapuram

J. Comput. Syst. Sci., 2007

Model Checking on Trees with Path Equivalences.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Instrumenting C Programs with Nested Word Monitors.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2007

CheckFence: checking consistency of concurrent data types on relaxed memory models.

[BibT_eX]

[DOI]

Sebastian Burckhardt

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Automata Based Interfaces for Control and Scheduling.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Symbolic Analysis for GSMP Models with One Stateful Clock.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

2006

Predicate abstraction for reachability analysis of hybrid systems.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2006

Modular strategies for recursive game graphs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Counterexample-guided predicate abstraction of hybrid systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Compositional modeling and refinement for hierarchical hybrid systems.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2006

A fixpoint calculus for local and global program flows.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

Preserving Secrecy Under Refinement.

[BibT_eX]

[DOI]

Steve Zdancewic

Proceedings of the Automata, Languages and Programming, 33rd International Colloquium, 2006

Bounded Model Checking for GSMP Models of Stochastic Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 9th International Workshop, 2006

Branching Pushdown Tree Automata.

[BibT_eX]

[DOI]

Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006

Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study.

[BibT_eX]

[DOI]

Sebastian Burckhardt

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Languages of Nested Trees.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2006

2005

Analysis of recursive state machines.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2005

Preface.

[BibT_eX]

[DOI]

Insup Lee

ACM Trans. Embed. Comput. Syst., 2005

Realizability and verification of MSC graphs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Symbolic computational techniques for solving games.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2005

Deciding Global Partial-Order Properties.

[BibT_eX]

[DOI]

Kenneth L. McMillan

Formal Methods Syst. Des., 2005

Trends and Challenges in Algorithmic Software Verification.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement.

[BibT_eX]

[DOI]

Sebastian Burckhardt

Proceedings of the Verification, 2005

On-the-Fly Reachability and Cycle Detection for Recursive State Machines.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Quantifying the Gap between Embedded Control Models and Time-Triggered Implementations.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE Real-Time Systems Symposium (RTSS 2005), 2005

Synthesis of interface specifications for Java classes.

[BibT_eX]

[DOI]

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Congruences for Visibly Pushdown Languages.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

Perturbed Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 8th International Workshop, 2005

The Benefits of Exposing Calls and Returns.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

Symbolic Compositional Verification by Learning Assumptions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Modular refinement of hierarchic reactive machines.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2004

Deterministic generators and games for Ltl fragments.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2004

Optimal paths in weighted timed automata.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2004

Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2004

Polyhedral Flows in Hybrid Automata.

[BibT_eX]

[DOI]

Sampath Kannan

Formal Methods Syst. Des., 2004

A Temporal Logic of Nested Calls and Returns.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Visibly pushdown languages.

[BibT_eX]

[DOI]

Proceedings of the 36th Annual ACM Symposium on Theory of Computing, 2004

Decision Problems for Timed Automata: A Survey.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for the Design of Real-Time Systems, 2004

Optimal Reachability for Weighted Timed Games.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

Structured Modeling of Concurrent Stochastic Hybrid Systems.

[BibT_eX]

[DOI]

Raman Sharykin

Proceedings of the Formal Techniques, 2004

Variable Reuse for Efficient Image Computation.

[BibT_eX]

[DOI]

Zijiang Yang

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

A model-based approach to integrating security policies for embedded devices.

[BibT_eX]

[DOI]

Michael McDougall

Carl A. Gunter

Proceedings of the EMSOFT 2004, 2004

Games for Formal Design and Verification of Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003

Inference of Message Sequence Charts.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2003

Hierarchical modeling and analysis of embedded systems.

[BibT_eX]

[DOI]

Proc. IEEE, 2003

Counter-Example Guided Predicate Abstraction of Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Generating embedded software from hierarchical hybrid models.

[BibT_eX]

[DOI]

Proceedings of the 2003 Conference on Languages, 2003

Progress on Reachability Analysis of Hybrid Systems Using Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 2003

Playing Games with Boxes and Diamonds.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2003, 2003

Compression of Partially Ordered Strings.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2003, 2003

Modular Strategies for Infinite Games on Recursive Graphs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Formal Analysis of Hierarchical State Machines.

[BibT_eX]

[DOI]

Proceedings of the Verification: Theory and Practice, 2003

2002

Alternating-time temporal logic.

[BibT_eX]

[DOI]

Orna Kupferman

J. ACM, 2002

A Framework and Architecture for Multi-Robot Coordination.

[BibT_eX]

[DOI]

Int. J. Robotics Res., 2002

Modeling and analyzing biomolecular networks.

[BibT_eX]

[DOI]

Comput. Sci. Eng., 2002

Reachability Analysis of Hybrid Systems via Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 5th International Workshop, 2002

Visual Programming for Modeling and Simulation of Biomolecular Regulatory Networks.

[BibT_eX]

[DOI]

Proceedings of the High Performance Computing, 2002

Exploiting Behavioral Hierarchy for Efficient Model Checking.

[BibT_eX]

[DOI]

Michael McDougall

Zijiang Yang

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Predictable programs in barcodes.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Compilers, 2002

2001

Model checking of hierarchical state machines.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2001

Parametric temporal logic for "model measuring".

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2001

Partial-Order Reduction in Symbolic State-Space Exploration.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

Shared Variables Interaction Diagrams.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001

JMOCHA: A Model Checking Tool that Exploits Design Structure.

[BibT_eX]

[DOI]

Proceedings of the 23rd International Conference on Software Engineering, 2001

Compositional Refinement for Hierarchical Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 4th International Workshop, 2001

Hybrid Modeling and Simulation of Biomolecular Networks.

[BibT_eX]

[DOI]

Calin Belta

Proceedings of the Hybrid Systems: Computation and Control, 4th International Workshop, 2001

Hierarchical Hybrid Modeling of Embedded Systems.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, First International Workshop, 2001

Heuristics for Hierarchical Partitioning with Application to Model Checking.

[BibT_eX]

[DOI]

M. Oliver Möller

Proceedings of the Correct Hardware Design and Verification Methods, 2001

Verifying Network Protocol Implementations by Symbolic Refinement Checking.

[BibT_eX]

[DOI]

Bow-Yaw Wang

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

Analysis of Recursive State Machines.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Computer-aided verification of reactive systems.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 2000

Discrete abstractions of hybrid systems.

[BibT_eX]

[DOI]

Proc. IEEE, 2000

Model-Checking of Correctness Conditions for Concurrent Objects.

[BibT_eX]

[DOI]

Kenneth L. McMillan

Inf. Comput., 2000

A Framework and Architecture for Multirobot Coordination.

[BibT_eX]

[DOI]

Proceedings of the Experimental Robotics VII [ISER 2000, 2000

Modular Specification of Hybrid Systems in CHARON.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, Third International Workshop, 2000

Automated Refinement Checking for Asynchronous Processes.

[BibT_eX]

[DOI]

Bow-Yaw Wang

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Exploiting Hierarchical Structure for Efficient Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2000, 2000

Efficient Reachability Analysis of Hierarchical Reactive Machines.

[BibT_eX]

[DOI]

Michael McDougall

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Event-Clock Automata: A Determinizable Class of Timed Automata.

[BibT_eX]

[DOI]

Limor Fix

Theor. Comput. Sci., 1999

Undecidability of Partial Order Logics.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1999

Reactive Modules.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1999

Introduction.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1999

Communicating Hierarchical State Machines.

[BibT_eX]

[DOI]

Sampath Kannan

Proceedings of the Automata, 1999

Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination.

[BibT_eX]

[DOI]

Proceedings of the FM'99 - Formal Methods, 1999

Model Checking of Message Sequence Charts.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '99: Concurrency Theory, 1999

"Next" Heuristic for On-the-Fly Model Checking.

[BibT_eX]

[DOI]

Bow-Yaw Wang

Proceedings of the CONCUR '99: Concurrency Theory, 1999

Automating Modular Verification.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '99: Concurrency Theory, 1999

Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998

Finitary Fairness.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 1998

Symbolic Exploration of transition Hierarchies.

[BibT_eX]

[DOI]

Sriram K. Rajamani

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

Membership Questions for Timed and Hybrid Automata.

[BibT_eX]

[DOI]

Robert P. Kurshan

Mahesh Viswanathan

Proceedings of the 19th IEEE Real-Time Systems Symposium, 1998

Efficient Formal Verification of Hierarchical Descriptions.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1998

Performance Evaluation and Prediction.

[BibT_eX]

[DOI]

Allen D. Malony

Proceedings of the Euro-Par '98 Parallel Processing, 1998

Alternating Refinement Relations.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '98: Concurrency Theory, 1998

MOCHA: Modularity in Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

Real-Time System = Discrete System + Clock Variables.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 1997

Time-Adaptive Algorithms for Synchronization.

[BibT_eX]

[DOI]

Hagit Attiya

SIAM J. Comput., 1997

Computing Accumulated Delays in Real-time Systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1997

Model-Checking of Real-Time Systems: A Telecommunications Application (Experience Report).

[BibT_eX]

[DOI]

Lalita Jategaonkar Jagadeesan

Joseph J. Kott

James Von Olnhausen

Proceedings of the Pulling Together, 1997

Modularity for Timed and Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '97: Concurrency Theory, 1997

1996

Automatic Symbolic Verification of Embedded Systems.

[BibT_eX]

[DOI]

Pei-Hsin Ho

IEEE Trans. Software Eng., 1996

An Analyzer for Message Sequence Charts.

[BibT_eX]

Gerard J. Holzmann

Softw. Concepts Tools, 1996

The Benefits of Relaxing Punctuality.

[BibT_eX]

[DOI]

Tomás Feder

J. ACM, 1996

Contention-Free Complexity of Shared Memory Algorithms.

[BibT_eX]

[DOI]

Inf. Comput., 1996

Fast Timing-Based Algorithms.

[BibT_eX]

[DOI]

Distributed Comput., 1996

Next Steps in Formal Verification.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

An Analyser for Mesage Sequence Charts.

[BibT_eX]

[DOI]

Gerard J. Holzmann

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

Verifying Abstractions of Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '96, 1996

1995

Timing Verification by Successive Approximation

[BibT_eX]

[DOI]

Inf. Comput., April, 1995

The Algorithmic Analysis of Hybrid Systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1995

Distinguishing tests for nondeterministic and probabilistic machines.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory of Computing, 1995

Model-Checking of Causality Properties

[BibT_eX]

[DOI]

Wojciech Penczek

Proceedings of the Proceedings, 1995

Timing Analysis in COSPAN.

[BibT_eX]

[DOI]

Robert P. Kurshan

Proceedings of the Hybrid Systems III: Verification and Control, 1995

Local Liveness for Compositional Modeling of Fair Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 1995

1994

A Theory of Timed Automata.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1994

A Really Temporal Logic.

[BibT_eX]

[DOI]

J. ACM, 1994

The Observational Power of Clocks.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '94, 1994

A Determinizable Class of Timed Automata.

[BibT_eX]

[DOI]

Limor Fix

Proceedings of the Computer Aided Verification, 6th International Conference, 1994

1993

Real-Time Logics: Complexity and Expressiveness

[BibT_eX]

[DOI]

Inf. Comput., May, 1993

Model-Checking in Dense Real-time

[BibT_eX]

[DOI]

Inf. Comput., May, 1993

Parametric real-time reasoning.

[BibT_eX]

[DOI]

Moshe Y. Vardi

Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, 1993

How to Share an Object: A Fast Timing-Based Solution.

[BibT_eX]

[DOI]

Proceedings of the Fifth IEEE Symposium on Parallel and Distributed Processing, 1993

1992

Results about Fast Mutual Exclusion.

[BibT_eX]

[DOI]

Proceedings of the Real-Time Systems Symposium, 1992

An implementation of three algorithms for timing verification based on automata emptiness.

[BibT_eX]

[DOI]

Proceedings of the Real-Time Systems Symposium, 1992

Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems, 1992

Back to the Future: Towards a Theory of Timed Regular Languages

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual Symposium on Foundations of Computer Science, 1992

Minimization of Timed Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '92, 1992

1991

Techniques for automatic verification of real-time systems.

[BibT_eX]

[DOI]

PhD thesis, 1991

Logics and Models of Real Time: A Survey.

[BibT_eX]

[DOI]

Proceedings of the Real-Time: Theory in Practice, 1991

Verifying Automata Specifications of Probabilistic Real-time Systems.

[BibT_eX]

[DOI]

Proceedings of the Real-Time: Theory in Practice, 1991

Model-Checking for Probabilistic Real-Time Systems (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991

1990

Model-Checking for Real-Time Systems

[BibT_eX]

[DOI]

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

Automata For Modeling Real-Time Systems.

[BibT_eX]

[DOI]