Thomas A. Henzinger

Bernhard Kragl

Proceedings of the 28th EACSL Annual Conference on Computer Science Logic, 2020

Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.

[BibT_eX]

[DOI]

Proceedings of the 31st International Conference on Concurrency Theory, 2020

A Survey of Bidding Games on Graphs (Invited Paper).

[BibT_eX]

[DOI]

Proceedings of the 31st International Conference on Concurrency Theory, 2020

Refinement for Structured Concurrent Programs.

[BibT_eX]

[DOI]

Bernhard Kragl

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Continuous-Time Models for System Design and Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computing and Software Science - State of the Art and Perspectives, 2019

Quantitative Automata under Probabilistic Semantics.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2019

Infinite-duration Bidding Games.

[BibT_eX]

[DOI]

Ventsislav Chonev

J. ACM, 2019

Bidding Games on Markov Decision Processes.

[BibT_eX]

[DOI]

Proceedings of the Reachability Problems - 13th International Conference, 2019

Designing Worm-inspired Neural Networks for Interpretable Robotic Control.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Robotics and Automation, 2019

Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.

[BibT_eX]

[DOI]

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

Long-Run Average Behavior of Vector Addition Systems with States.

[BibT_eX]

[DOI]

Proceedings of the 30th International Conference on Concurrency Theory, 2019

Transient Memory in Gene Regulation.

[BibT_eX]

[DOI]

Proceedings of the Computational Methods in Systems Biology, 2019

Membership-Based Synthesis of Linear Hybrid Automata.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Run-Time Optimization for Learned Controllers Through Quantitative Games.

[BibT_eX]

[DOI]

Bettina Könighofer

Stefan Pranger

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Introduction to Model Checking.

[BibT_eX]

[DOI]

Edmund M. Clarke

Helmut Veith

Proceedings of the Handbook of Model Checking., 2018

Contracts for System Design.

[BibT_eX]

[DOI]

Werner Damm

Kim G. Larsen

Found. Trends Electron. Des. Autom., 2018

Infinite-Duration Poorman-Bidding Games.

[BibT_eX]

[DOI]

Rasmus Ibsen-Jensen

Proceedings of the Web and Internet Economics - 14th International Conference, 2018

A Theory of Register Monitors.

[BibT_eX]

[DOI]

Thomas Ferrère

N. Ege Saraç

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Monitoring Temporal Logic with Clock Variables.

[BibT_eX]

[DOI]

Adrián Elgyütt

Thomas Ferrère

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

The first-order logic of signals: keynote.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Embedded Software, 2018

Synchronizing the Asynchronous.

[BibT_eX]

[DOI]

Bernhard Kragl

Proceedings of the 29th International Conference on Concurrency Theory, 2018

Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes.

[BibT_eX]

[DOI]

Hui Kong

Ezio Bartocci

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Space-Time Interpolants.

[BibT_eX]

[DOI]

Goran Frehse

Mirco Giacobbe

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Computing Average Response Time.

[BibT_eX]

[DOI]

Proceedings of the Principles of Modeling, 2018

Temporal Logics for Multi-Agent Systems.

[BibT_eX]

[DOI]

Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, 2018

2017

Faster Statistical Model Checking for Unbounded Temporal Properties.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2017

Nested Weighted Automata.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2017

Edit Distance for Pushdown Automata.

[BibT_eX]

[DOI]

Rasmus Ibsen-Jensen

Log. Methods Comput. Sci., 2017

Quantitative fair simulation games.

[BibT_eX]

[DOI]

Yaron Velner

Inf. Comput., 2017

Preface of the Special Issue in Memoriam Helmut Veith.

[BibT_eX]

[DOI]

Georg Gottlob

Georg Weissenbacher

Formal Methods Syst. Des., 2017

From non-preemptive to preemptive scheduling using synchronization synthesis.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Model checking the evolution of gene regulatory networks.

[BibT_eX]

[DOI]

Acta Informatica, 2017

Counterexample-Guided Refinement of Template Polyhedra.

[BibT_eX]

[DOI]

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

Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults.

[BibT_eX]

[DOI]

Shubham Goel

Guillermo Rodríguez-Navas

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

The quest for average response time.

[BibT_eX]

[DOI]

Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, 2017

Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017

Conic Abstractions for Hybrid Systems.

[BibT_eX]

[DOI]

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

Bidirectional Nested Weighted Automata.

[BibT_eX]

[DOI]

Proceedings of the 28th International Conference on Concurrency Theory, 2017

Challenges and Tool Implementation of Hybrid Rapidly-Exploring Random Trees.

[BibT_eX]

[DOI]

Proceedings of the Numerical Software Verification - 10th International Workshop, 2017

The Cost of Exactness in Quantitative Reachability.

[BibT_eX]

[DOI]

Proceedings of the Models, Algorithms, Logics and Tools, 2017

2016

Viewpoints on "Logic activities in Europe", twenty years later.

[BibT_eX]

[DOI]

Bull. EATCS, 2016

Invariant Clusters for Hybrid Systems.

[BibT_eX]

[DOI]

CoRR, 2016

Adaptive moment closure for parameter inference of biochemical reaction networks.

[BibT_eX]

[DOI]

Biosyst., 2016

Lipschitz Robustness of Timed I/O Systems.

[BibT_eX]

[DOI]

Roopsha Samanta

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Abstraction-driven Concolic Testing.

[BibT_eX]

[DOI]

Przemyslaw Daca

Ashutosh Gupta

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Quantitative Monitor Automata.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 23rd International Symposium, 2016

PSync: a partially synchronous language for fault-tolerant distributed algorithms.

[BibT_eX]

[DOI]

Cezara Dragoi

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Nested Weighted Limit-Average Automata of Bounded Width.

[BibT_eX]

[DOI]

Proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science, 2016

Scalable Static Hybridization Methods for Analysis of Nonlinear Systems.

[BibT_eX]

[DOI]

Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016

Discrete Abstraction of Multiaffine Systems.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems Biology - 5th International Workshop, 2016

Local Linearizability for Concurrent Container-Type Data Structures.

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Concurrency Theory, 2016

Linear Distances between Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Concurrency Theory, 2016

Array Folds Logic.

[BibT_eX]

[DOI]

Przemyslaw Daca

Andrey Kupriyanov

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Guest Editors' Introduction to Special Issue on Computational Methods in Systems Biology.

[BibT_eX]

[DOI]

Ashutosh Gupta

ACM Trans. Model. Comput. Simul., 2015

Theory in practice for system design and verification.

[BibT_eX]

[DOI]

Moshe Y. Vardi

ACM SIGLOG News, 2015

Measuring and Synthesizing Systems in Probabilistic Environments.

[BibT_eX]

[DOI]

Rohit Singh

J. ACM, 2015

The complexity of multi-mean-payoff and multi-energy games.

[BibT_eX]

[DOI]

Yaron Velner

Alexander Moshe Rabinovich

Inf. Comput., 2015

Randomness for free.

[BibT_eX]

[DOI]

Hugo Gimbert

Inf. Comput., 2015

Local Linearizability.

[BibT_eX]

[DOI]

CoRR, 2015

Aspect-oriented linearizability proofs.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2015

Optimizing Solution Quality in Synchronization Synthesis.

[BibT_eX]

[DOI]

CoRR, 2015

The equivalence problem for finite automata: technical perspective.

[BibT_eX]

[DOI]

Commun. ACM, 2015

Model Checking Gene Regulatory Networks.

[BibT_eX]

[DOI]

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

The Need for Language Support for Fault-Tolerant Distributed Systems.

[BibT_eX]

[DOI]

Cezara Dragoi

Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Succinct Representation of Concurrent Trace Sets.

[BibT_eX]

[DOI]

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

The Target Discounted-Sum Problem.

[BibT_eX]

[DOI]

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Segment Abstraction for Worst-Case Execution Time Analysis.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2015

Complete Composition Operators for IOCO-Testing Theory.

[BibT_eX]

[DOI]

Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering, 2015

2014

Temporal Specifications with Accumulative Values.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2014

Interface simulation distances.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2014

Abstractions from proofs.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 2014

Exact and Approximate Determinization of Discounted-Sum Automata.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2014

Synthesizing robust systems.

[BibT_eX]

[DOI]

Acta Informatica, 2014

A Logic-Based Framework for Verifying Consensus Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

Battery transition systems.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Compositional Specifications for ioco Testing.

[BibT_eX]

[DOI]

Proceedings of the Seventh IEEE International Conference on Software Testing, 2014

Probabilistic programming.

[BibT_eX]

[DOI]

Proceedings of the on Future of Software Engineering, 2014

Model measuring for hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2014

Lipschitz Robustness of Finite-state Transducers.

[BibT_eX]

[DOI]

Roopsha Samanta

Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014

Computer-aided verification technology for biology.

[BibT_eX]

[DOI]

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

Regression-Free Synthesis for Concurrency.

[BibT_eX]

[DOI]

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

2013

The Propagation Approach for Computing Biochemical Reaction Networks.

[BibT_eX]

[DOI]

Maria Mateescu

IEEE ACM Trans. Comput. Biol. Bioinform., 2013

Synthesis of AMBA AHB from formal specification: a case study.

[BibT_eX]

[DOI]

Yashdeep Godhal

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

Strategy improvement for concurrent reachability and turn-based stochastic safety games.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2013

Quantitative reactive modeling and verification.

[BibT_eX]

[DOI]

Comput. Sci. Res. Dev., 2013

A survey of partial-observation stochastic parity games.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

Quantitative relaxation of concurrent data structures.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Quantitative abstraction refinement.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Quantitative Fitness Measures for Embedded Systems.

[BibT_eX]

Proceedings of the PECCS 2013, 2013

Distributed synthesis for LTL fragments.

[BibT_eX]

[DOI]

Andreas Pavlogiannis

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

The Ackermann Award 2013.

[BibT_eX]

[DOI]

Anuj Dawar

Damian Niwinski

Proceedings of the Computer Science Logic 2013 (CSL 2013), 2013

Aspect-Oriented Linearizability Proofs.

[BibT_eX]

[DOI]

Ali Sezgin

Viktor Vafeiadis

Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

From Model Checking to Model Measuring.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

Distributed queues in shared memory: multicore performance and scalability through quantitative relaxation.

[BibT_eX]

[DOI]

Proceedings of the Computing Frontiers Conference, 2013

Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.

[BibT_eX]

[DOI]

Cezara Dragoi

Ashutosh Gupta

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Efficient Synthesis for Concurrency by Semantics-Preserving Transformations.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Lumpability abstractions of rule-based systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2012

Simulation distances.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2012

Separate compilation of hierarchical real-time programs into linear-bounded Embedded Machine code.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2012

A survey of stochastic ω-regular games.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2012

2011 CAV award announcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2012

Finite Automata with Time-Delay Blocks (Extended Version)

[BibT_eX]

[DOI]

CoRR, 2012

Strategy Improvement for Concurrent Reachability and Safety Games

[BibT_eX]

[DOI]

CoRR, 2012

Keynote on "the propagation approach for computing biochemical reaction networks".

[BibT_eX]

[DOI]

Proceedings of the Winter Simulation Conference, 2012

Ideal Abstractions for Well-Structured Transition Systems.

[BibT_eX]

[DOI]

Thomas Wies

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Conditional model checking: a technique to pass information between verifiers.

[BibT_eX]

[DOI]

Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 2012

Independent Implementability of Viewpoints.

[BibT_eX]

[DOI]

Dejan Nickovic

Proceedings of the Large-Scale Complex IT Systems. Development, Operation and Management, 2012

Quantitative Reactive Models.

[BibT_eX]

[DOI]

Proceedings of the Model Driven Engineering Languages and Systems, 2012

Approximate Determinization of Quantitative Automata.

[BibT_eX]

[DOI]

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

Synchronous Interface Theories and Time Triggered Scheduling.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2012

Finite automata with time-delay blocks.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Embedded Software, 2012

Synthesis from incompatible specifications.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Embedded Software, 2012

Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits.

[BibT_eX]

[DOI]

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

2011

A Theory of Synchronous Relational Interfaces.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2011

Qualitative concurrent parity games.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2011

Approximation of event probabilities in noisy cellular processes.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

Formalisms for Specifying Markovian Population Models.

[BibT_eX]

[DOI]

Verena Wolf

Int. J. Found. Comput. Sci., 2011

Verification of STM on relaxed memory models.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2011

Conditional Model Checking

[BibT_eX]

[DOI]

CoRR, 2011

The Decidability Frontier for Probabilistic Automata on Infinite Words

[BibT_eX]

[DOI]

Mathieu Tracol

CoRR, 2011

Timed Parity Games: Complexity and Robustness

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2011

Biology as reactivity.

[BibT_eX]

[DOI]

Jasmin Fisher

David Harel

Commun. ACM, 2011

QUASY: Quantitative Synthesis Tool.

[BibT_eX]

[DOI]

Rohit Singh

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

Specification-centered robustness.

[BibT_eX]

[DOI]

Karin Greimel

Proceedings of the Industrial Embedded Systems (SIES), 2011

Quantitative Evaluation of BFT Protocols.

[BibT_eX]

[DOI]

Raluca Halalai

Proceedings of the Eighth International Conference on Quantitative Evaluation of Systems, 2011

The Complexity of Request-Response Games.

[BibT_eX]

[DOI]

Florian Horn

Proceedings of the Language and Automata Theory and Applications, 2011

Static Scheduling in Clouds.

[BibT_eX]

[DOI]

Proceedings of the 3rd USENIX Workshop on Hot Topics in Cloud Computing, 2011

Scheduling large jobs by abstraction refinement.

[BibT_eX]

[DOI]

Proceedings of the European Conference on Computer Systems, 2011

From boolean to quantitative synthesis.

[BibT_eX]

[DOI]

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

Determinizing Discounted-Sum Automata.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2011

The Complexity of Quantitative Information Flow Problems.

[BibT_eX]

[DOI]

Proceedings of the 24th IEEE Computer Security Foundations Symposium, 2011

Dynamic Reactive Modules.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Propagation models for computing biochemical reaction networks.

[BibT_eX]

[DOI]

Maria Mateescu

Proceedings of the Computational Methods in Systems Biology, 9th International Conference, 2011

Quantitative Synthesis for Concurrent Programs.

[BibT_eX]

[DOI]

Rohit Singh

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

Quantitative languages.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2010

Strategy logic.

[BibT_eX]

[DOI]

Inf. Comput., 2010

Strategy construction for parity games with imperfect information.

[BibT_eX]

[DOI]

Dietmar Berwanger

Martin De Wulf

Inf. Comput., 2010

Model checking transactional memories.

[BibT_eX]

[DOI]

Distributed Comput., 2010

Expressiveness and Closure Properties for Quantitative Languages

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2010

Synthesis of AMBA AHB from Formal Specification

[BibT_eX]

[DOI]

Yashdeep Godhal

CoRR, 2010

Solving the chemical master equation using sliding windows.

[BibT_eX]

[DOI]

BMC Syst. Biol., 2010

Invariant and Type Inference for Matrices.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Transactions in the jungle.

[BibT_eX]

[DOI]

Proceedings of the SPAA 2010: Proceedings of the 22nd Annual ACM Symposium on Parallelism in Algorithms and Architectures, 2010

SABRE: A Tool for Stochastic Analysis of Biochemical Reaction Networks.

[BibT_eX]

[DOI]

Proceedings of the QEST 2010, 2010

From Boolean to quantitative notions of correctness.

[BibT_eX]

[DOI]

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Qualitative Analysis of Partially-Observable Markov Decision Processes.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2010, 2010

Aligators for Arrays (Tool Paper).

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

ABC: Algebraic Bound Computation for Loops.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Generalized Mean-payoff and Energy Games.

[BibT_eX]

[DOI]

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

Forward Analysis of Depth-Bounded Processes.

[BibT_eX]

[DOI]

Thomas Wies

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

Shape Refinement through Explicit Heap Analysis.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2010

A marketplace for cloud resources.

[BibT_eX]

[DOI]

Proceedings of the 10th International conference on Embedded software, 2010

Mean-Payoff Automaton Expressions.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

Hybrid numerical solution of the chemical master equation.

[BibT_eX]

[DOI]

Proceedings of the Computational Methods in Systems Biology, 8th International Conference, 2010

Gist: A Solver for Probabilistic Games.

[BibT_eX]

[DOI]

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

Robustness in the Presence of Liveness.

[BibT_eX]

[DOI]

Karin Greimel

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

Quantitative Simulation Games.

[BibT_eX]

[DOI]

Proceedings of the Time for Verification, 2010

Probabilistic Automata on Infinite Words: Decidability and Undecidability Results.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2010

Robustness of Sequential Circuits.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Application of Concurrency to System Design, 2010

FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Conference on Cloud Computing, 2010

2009

Finitary winning in omega-regular games.

[BibT_eX]

[DOI]

Florian Horn

ACM Trans. Comput. Log., 2009

The 2008 CAV Award citation.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2009

Alpaga: A Tool for Solving Parity Games with Imperfect Information.

[BibT_eX]

[DOI]

Dietmar Berwanger

Martin De Wulf

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

Termination criteria for solving concurrent safety and reachability games.

[BibT_eX]

[DOI]

Proceedings of the Twentieth Annual ACM-SIAM Symposium on Discrete Algorithms, 2009

Distributed, Modular HTL.

[BibT_eX]

[DOI]

Eduardo R. B. Marques

Ana Sokolova

Proceedings of the 30th IEEE Real-Time Systems Symposium, 2009

Stochastic Games with Finitary Objectives.

[BibT_eX]

[DOI]

Florian Horn

Proceedings of the Mathematical Foundations of Computer Science 2009, 2009

A Survey of Stochastic Games with Limsup and Liminf Objectives.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 36th Internatilonal Colloquium, 2009

Synthesizing robust systems.

[BibT_eX]

[DOI]

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Alternating Weighted Automata.

[BibT_eX]

[DOI]

Proceedings of the Fundamentals of Computation Theory, 17th International Symposium, 2009

On relational interfaces.

[BibT_eX]

[DOI]

Proceedings of the 9th ACM & IEEE International conference on Embedded software, 2009

Probabilistic Weighted Automata.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

Sliding Window Abstraction for Infinite Markov Chains.

[BibT_eX]

[DOI]

Maria Mateescu

Verena Wolf

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

Software Transactional Memory on Relaxed Memory Models.

[BibT_eX]

[DOI]

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

Better Quality in Synthesis through Quantitative Objectives.

[BibT_eX]

[DOI]

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

2008

Reduction of stochastic parity to stochastic mean-payoff games.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2008

Stochastic limit-average games are in EXPTIME.

[BibT_eX]

[DOI]

Int. J. Game Theory, 2008

Equivalence of Labeled Markov Chains.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2008

Algorithms for Büchi Games

[BibT_eX]

[DOI]

CoRR, 2008

Strategy Improvement for Concurrent Safety Games

[BibT_eX]

[DOI]

CoRR, 2008

Permissiveness in Transactional Memories.

[BibT_eX]

[DOI]

Proceedings of the Distributed Computing, 22nd International Symposium, 2008

Value Iteration.

[BibT_eX]

[DOI]

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

Proving non-termination.

[BibT_eX]

[DOI]

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Model checking transactional memories.

[BibT_eX]

[DOI]

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

Valigator: A Verification Tool with Bound and Invariant Generation.

[BibT_eX]

[DOI]

Thibaud Hottelier

Laura Kovács

Proceedings of the Logic for Programming, 2008

Program Analysis with Dynamic Precision Adjustment.

[BibT_eX]

[DOI]

Grégory Théoduloz

Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

Controller Synthesis with Budget Constraints.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008

Trading Infinite Memory for Uniform Randomness in Timed Games.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008

Model-Checking omega-Regular Properties of Interval Markov Chains.

[BibT_eX]

[DOI]

Koushik Sen

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

Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Systems Biology, First International Workshop, 2008

Interface theories with component reuse.

[BibT_eX]

[DOI]

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

Logical Reliability of Interacting Real-Time Tasks.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2008

Completeness and Nondeterminism in Model Checking Transactional Memories.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

Environment Assumptions for Synthesis.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

Strategy Construction for Parity Games with Imperfect Information.

[BibT_eX]

[DOI]

Dietmar Berwanger

Sangram Raje

Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

2007

The embedded machine: Predictable, portable real-time code.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2007

Concurrent reachability games.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

The software model checker Blast.

[BibT_eX]

[DOI]

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

Predictive Modeling of Signaling Crosstalk during C. elegans Vulval Development.

[BibT_eX]

[DOI]

PLoS Comput. Biol., 2007

Algorithms for Omega-Regular Games with Imperfect Information.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2007

The Discipline of Embedded Systems Design.

[BibT_eX]

[DOI]

Joseph Sifakis

Computer, 2007

Qualitative networks: a symbolic approach to analyze biological signaling networks.

[BibT_eX]

[DOI]

Marc A. Schaub

Jasmin Fisher

BMC Syst. Biol., 2007

Invariant Synthesis for Combined Theories.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2007

Assume-Guarantee Synthesis.

[BibT_eX]

[DOI]

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

Games, Time, and Probability: Graph Models for System Design and Analysis.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2007: Theory and Practice of Computer Science, 2007

Path invariants.

[BibT_eX]

[DOI]

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

Probabilistic Systems with LimSup and LimInf Objectives.

[BibT_eX]

[DOI]

Proceedings of the Infinity in Logic and Computation, International Conference, 2007

An Application ofWeb-Service Interfaces.

[BibT_eX]

[DOI]

Proceedings of the 2007 IEEE International Conference on Web Services (ICWS 2007), 2007

Minimum-Time Reachability in Timed Games.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 34th International Colloquium, 2007

Generalized Parity Games.

[BibT_eX]

[DOI]

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

Quantitative Generalizations of Languages.

[BibT_eX]

[DOI]

Proceedings of the Developments in Language Theory, 11th International Conference, 2007

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis.

[BibT_eX]

[DOI]

Grégory Théoduloz

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Algorithms for Interface Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

On the universal and existential fragments of the mu-calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Games with secure equilibria.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Executable biology.

[BibT_eX]

[DOI]

Jasmin Fisher

Proceedings of the Winter Simulation Conference WSC 2006, 2006

Finitary Winning in omega-Regular Games.

[BibT_eX]

[DOI]

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

Markov Decision Processes with Multiple Objectives.

[BibT_eX]

[DOI]

Proceedings of the STACS 2006, 2006

Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games.

[BibT_eX]

[DOI]

Proceedings of the STACS 2006, 2006

The complexity of quantitative concurrent parity games.

[BibT_eX]

[DOI]

Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms, 2006

SYNERGY: a new algorithm for property checking.

[BibT_eX]

[DOI]

Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006

An Interface Algebra for Real-Time Components.

[BibT_eX]

[DOI]

Proceedings of the 12th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2006), 2006

Strategy Improvement for Concurrent Reachability Games.

[BibT_eX]

[DOI]

Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006

Compositional Quantitative Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006

Timed Alternating-Time Temporal Logic.

[BibT_eX]

[DOI]

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

The Embedded Systems Design Challenge.

[BibT_eX]

[DOI]

Joseph Sifakis

Proceedings of the FM 2006: Formal Methods, 2006

A hierarchical coordination language for interacting real-time tasks.

[BibT_eX]

[DOI]

Arkadeb Ghosal

Daniel T. Iercan

Proceedings of the 6th ACM & IEEE International conference on Embedded software, 2006

Solving Games Without Determinization.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 20th International Workshop, 2006

Algorithms for Omega-Regular Games with Imperfect Information, .

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 20th International Workshop, 2006

Strategy Improvement for Stochastic Rabin and Streett Games.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2006 - Concurrency Theory, 17th International Conference, 2006

Antichains: A New Algorithm for Checking Universality of Finite Automata.

[BibT_eX]

[DOI]

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

Lazy Shape Analysis.

[BibT_eX]

[DOI]

Grégory Théoduloz

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

Abstract Counterexample-Based Refinement for Powerset Domains.

[BibT_eX]

[DOI]

Proceedings of the Program Analysis and Compilation, 2006

2005

A classification of symbolic transition systems.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2005

Model checking discounted temporal properties.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Web service interfaces.

[BibT_eX]

[DOI]

Arindam Chakrabarti

Proceedings of the 14th international conference on World Wide Web, 2005

A programmable microkernel for real-time systems.

[BibT_eX]

[DOI]

Marco A. A. Sanvido

Proceedings of the 1st International Conference on Virtual Execution Environments, 2005

Counterexample-guided Planning.

[BibT_eX]

[DOI]

Proceedings of the UAI '05, 2005

Games in system design and verification.

[BibT_eX]

[DOI]

Proceedings of the 10th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-2005), 2005

The BLAST Software Verification System.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2005

Permissive interfaces.

[BibT_eX]

[DOI]

Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005

Trading End-to-End Latency for Composability.

[BibT_eX]

[DOI]

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

Mean-Payoff Parity Games.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Composable code generation for distributed giotto.

[BibT_eX]

[DOI]

Proceedings of the 2005 ACM SIGPLAN/SIGBED Conference on Languages, 2005

The Complexity of Stochastic Rabin and Streett Games'.

[BibT_eX]

[DOI]

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

Semiperfect-Information Games.

[BibT_eX]

[DOI]

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

Quantifying Similarities Between Timed Systems.

[BibT_eX]

[DOI]

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

Automatic Rectangular Refinement of Affine Hybrid Systems.

[BibT_eX]

[DOI]

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

Checking Memory Safety with Blast.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2005

Verifying Quantitative Properties Using Bound Functions.

[BibT_eX]

[DOI]

Arindam Chakrabarti

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004

Stack size analysis for interrupt-driven programs.

[BibT_eX]

[DOI]

Inf. Comput., 2004

Quantitative stochastic parity games.

[BibT_eX]

[DOI]

Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, 2004

The Blast Query Language for Software Verification..

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 11th International Symposium, 2004

Trading Memory for Randomness.

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), 2004

Race checking by context inference.

[BibT_eX]

[DOI]

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

Invited talk: the blast query language for software verification.

[BibT_eX]

[DOI]

Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

An Eclipse Plug-in for Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 12th International Workshop on Program Comprehension (IWPC 2004), 2004

Generating Tests from Counterexamples.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004

Event-Driven Programming with Logical Execution Times.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 7th International Workshop, 2004

A typed assembly language for real-time programs.

[BibT_eX]

[DOI]

Proceedings of the EMSOFT 2004, 2004

Rich Interfaces for Software Modules.

[BibT_eX]

[DOI]

Proceedings of the ECOOP 2004, 2004

Embedded Software: Better Models, Better Code.

[BibT_eX]

[DOI]

Proceedings of the Applications and Theory of Petri Nets 2004, 2004

2003

Giotto: a time-triggered language for embedded programming.

[BibT_eX]

[DOI]

Benjamin Horowitz

Proc. IEEE, 2003

From Pre-Historic to Post-Modern Symbolic Model Checking.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2003

Automata for Specifying Component Interfaces.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 2003

On the Universal and Existential Fragments of the µ-Calculus.

[BibT_eX]

[DOI]

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

Software Verification with BLAST.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2003

Counterexample-Guided Control.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

Discounting the Future in Systems Theory.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

Schedule-Carrying Code.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, Third International Conference, 2003

Resource Interfaces.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, Third International Conference, 2003

Simple Stochastic Parity Games.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 17th International Workshop, 2003

The Element of Surprise in Timed Games.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2003, 2003

Thread-Modular Abstraction Refinement.

[BibT_eX]

[DOI]

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

Extreme Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Verification: Theory and Practice, 2003

Model Checking: From Hardware to Software.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, First Asian Symposium, 2003

2002

An assume-guarantee rule for checking simulation.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2002

Axioms for real-time logics.

[BibT_eX]

[DOI]

Pierre-Yves Schobbens

Theor. Comput. Sci., 2002

Alternating-time temporal logic.

[BibT_eX]

[DOI]

J. ACM, 2002

Fair Simulation.

[BibT_eX]

[DOI]

Inf. Comput., 2002

Lazy abstraction.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Convertibility verification and converter synthesis: two faces of the same coin.

[BibT_eX]

[DOI]

Roberto Passerone

Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, 2002

Synthesis of Uninitialized Systems.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 29th International Colloquium, 2002

From Models to Code: The Missing Link in Embedded Software.

[BibT_eX]

[DOI]

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

A Comparison of Control Problems for Timed and Hybrid Systems.

[BibT_eX]

[DOI]

Franck Cassez

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

A Giotto-Based Helicopter Control System.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, Second International Conference, 2002

Time-Safety Checking for Embedded Programs.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, Second International Conference, 2002

Timed Interfaces.

[BibT_eX]

[DOI]

Mariëlle Stoelinga

Proceedings of the Embedded Software, Second International Conference, 2002

Trading Probability for Fairness.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 16th International Workshop, 2002

Temporal-Safety Proofs for Systems Code.

[BibT_eX]

[DOI]

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

The Symbolic Approach to Hybrid Systems.

[BibT_eX]

[DOI]

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

Synchronous and Bidirectional Component Interfaces.

[BibT_eX]

[DOI]

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

Interface Compatibility Checking for Software Modules.

[BibT_eX]

[DOI]

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

2001

Partial-Order Reduction in Symbolic State-Space Exploration.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

MCWEB: A Model-Checking Tool for Web Site Debugging.

[BibT_eX]

[DOI]

Proceedings of the Poster Proceedings of the Tenth International World Wide Web Conference, 2001

Interface automata.

[BibT_eX]

[DOI]

Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, 2001

From Verification to Control: Dynamic Programs for Omega-Regular Objectives.

[BibT_eX]

[DOI]

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

Embedded Control Systems Development with Giotto.

[BibT_eX]

[DOI]

Benjamin Horowitz

Proceedings of The Workshop on Languages, 2001

JMOCHA: A Model Checking Tool that Exploits Design Structure.

[BibT_eX]

[DOI]

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

Hybrid Systems Applications: An Oxymoron?

[BibT_eX]

[DOI]

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

Assume-Guarantee Reasoning for Hierarchical Hybrid Systems.

[BibT_eX]

[DOI]

Marius Minea

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

Interface Theories for Component-Based Design.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, First International Workshop, 2001

The Control of Synchronous Systems, Part II.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2001, 2001

Symbolic Algorithms for Infinite-State Games.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2001, 2001

Compositional Methods for Probabilistic Systems.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2001, 2001

Some lessons from the HYTECH experience.

[BibT_eX]

[DOI]

Jörg Preußig

Proceedings of the 40th IEEE Conference on Decision and Control, 2001

2000

New directions in computer-aided verification.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 2000

Discrete abstractions of hybrid systems.

[BibT_eX]

[DOI]

Proc. IEEE, 2000

Exploiting Design Structure in Model Checking.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Models for Time-Critical Systems, 2000

Fair Bisimulation.

[BibT_eX]

[DOI]

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

Symbolic Model Checking for Rectangular Hybrid Systems.

[BibT_eX]

[DOI]

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

A Classification of Symbolic Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the STACS 2000, 2000

Abstract Interpretation of Game Properties.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 7th International Symposium, 2000

Concurrent Omega-Regular Games.

[BibT_eX]

[DOI]

Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

Masaccio: A Formal Model for Embedded Components.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 2000

Decomposing Refinement Proofs Using Assume-Guarantee Reasoning.

[BibT_eX]

[DOI]

Proceedings of the 2000 IEEE/ACM International Conference on Computer-Aided Design, 2000

Robust Undecidability of Timed and Hybrid Systems.

[BibT_eX]

[DOI]

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

Beyond HYTECH: Hybrid Systems Analysis Using Interval Numerical Methods.

[BibT_eX]

[DOI]

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

The Control of Synchronous Systems.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2000, 2000

Detecting Errors Before Reaching Them.

[BibT_eX]

[DOI]

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

1999

Discrete-Time Control for Rectangular Hybrid Automata.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1999

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

[BibT_eX]

[DOI]

Limor Fix

Theor. Comput. Sci., 1999

Reactive Modules.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1999

Introduction.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1999

Formal specification and verification of a dataflow processor array.

[BibT_eX]

[DOI]

Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Rectangular Hybrid Games.

[BibT_eX]

[DOI]

Benjamin Horowitz

Proceedings of the CONCUR '99: Concurrency Theory, 1999

Automating Modular Verification.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '99: Concurrency Theory, 1999

Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems.

[BibT_eX]

[DOI]

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

Assume-Guarantee Refinement Between Different Time Scales.

[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

Algorithmic analysis of nonlinear hybrid systems.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 1998

What's Decidable about Hybrid Automata?

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1998

Symbolic Exploration of transition Hierarchies.

[BibT_eX]

[DOI]

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

Computer-aided Verification of Embedded Systems.

[BibT_eX]

Proceedings of the Fundamentals - Foundations of Computer Science, 1998

The Regular Real-Time Languages.

[BibT_eX]

[DOI]

Pierre-Yves Schobbens

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Model Checking Game Properties of Multi-agent Systems (Abstract).

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Reachability Verification for Hybrid Automata.

[BibT_eX]

[DOI]

Vlad Rusu

Proceedings of the Hybrid Systems: Computation and Control, First International Workshop, 1998

An Algorithm for the Approximative Analysis of Rectangular Automata.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998

It's About Time: Real-Time Logics Reviewed.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '98: Concurrency Theory, 1998

Alternating Refinement Relations.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '98: Concurrency Theory, 1998

You Assume, We Guarantee: Methodology and Case Studies.

[BibT_eX]

[DOI]

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

From Pre-historic to Post-modern Symbolic Model Checking.

[BibT_eX]

[DOI]

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

MOCHA: Modularity in Model Checking.

[BibT_eX]

[DOI]

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

1997

HYTECH: A Model Checker for Hybrid Systems.

[BibT_eX]

[DOI]

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

Real-Time System = Discrete System + Clock Variables.

[BibT_eX]

[DOI]

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

Computing Accumulated Delays in Real-time Systems.

[BibT_eX]

[DOI]

Costas Courcoubetis

Formal Methods Syst. Des., 1997

From Quantity to Quality.

[BibT_eX]

[DOI]

Proceedings of the Hybrid and Real-Time Systems, 1997

Robust Timed Automata.

[BibT_eX]

[DOI]

Vineet Gupta

Radha Jagadeesan

Proceedings of the Hybrid and Real-Time Systems, 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]

IEEE Trans. Software Eng., 1996

The Benefits of Relaxing Punctuality.

[BibT_eX]

[DOI]

Tomás Feder

J. ACM, 1996

Some Myths About Formal Verification.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

The Theory of Hybrid Automata.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1996

A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking.

[BibT_eX]

[DOI]

Moshe Y. Vardi

Proceedings of the CONCUR '96, 1996

State Equivalences for Rectangular Hybrid Automata.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '96, 1996

1995

The Algorithmic Analysis of Hybrid Systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1995

A User Guide to HyTech.

[BibT_eX]

[DOI]

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

HyTech: The Next Generation.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE Real-Time Systems Symposium, 1995

The Expressive Power of Clocks.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 22nd International Colloquium, 1995

Hybrid Automata with Finite Bisimulatioins.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 22nd International Colloquium, 1995

Linear Phase-Portrait Approximations for Nonlinear Hybrid Systems.

[BibT_eX]

[DOI]

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

Computing Simulations on Finite and Infinite Graphs.

[BibT_eX]

[DOI]

Monika Rauch Henzinger

Proceedings of the 36th Annual Symposium on Foundations of Computer Science, 1995

Using HyTech to Synthesize Control Parameters for a Steam Boiler.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Applications, 1995

Algorithmic Analysis of Nonlinear Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 1995

Local Liveness for Compositional Modeling of Fair Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 1995

1994

Temporal Proof Methodologies for Timed Transition Systems

[BibT_eX]

[DOI]

Zohar Manna

Amir Pnueli

Inf. Comput., August, 1994

Symbolic Model Checking for Real-Time Systems

[BibT_eX]

[DOI]

Inf. Comput., June, 1994

A Really Temporal Logic.

[BibT_eX]

[DOI]

J. ACM, 1994

HYTECH: The Cornell HYbrid TECHnology Tool.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems II, 1994

A Note on Abstract Interpretation Strategies for Hybrid Automata.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems II, 1994

Prooving Safety Properties of Hybrid Systems.

[BibT_eX]

[DOI]

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

Verification Methods for the Divergent Runs of Clock Systems.

[BibT_eX]

[DOI]

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

The Observational Power of Clocks.

[BibT_eX]

[DOI]

Costas Courcoubetis

Proceedings of the CONCUR '94, 1994

A Determinizable Class of Timed Automata.

[BibT_eX]

[DOI]