Orna Kupferman

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

Good-Enough Synthesis.

[BibT_eX]

[DOI]

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

On (I/O)-Aware Good-For-Games Automata.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Flow Logic.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2019

A Parametrized Analysis of Algorithms on Hierarchical Graphs.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2019

Sensing as a Complexity Measure.

[BibT_eX]

[DOI]

Denis Kuperberg

Int. J. Found. Comput. Sci., 2019

Capacitated automata and systems.

[BibT_eX]

[DOI]

Inf. Comput., 2019

Multi-player flow games.

[BibT_eX]

[DOI]

Auton. Agents Multi Agent Syst., 2019

Minimizing GFG Transition-Based Automata.

[BibT_eX]

[DOI]

Bader Abu Radi

Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019

[BibT_eX]

[DOI]

Ayrat Khalimov

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

2018

Automata Theory and Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Model Checking., 2018

Synthesis from component libraries with costs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2018

An Abstraction-Refinement Methodologyfor Reasoning about Network Games†.

[BibT_eX]

[DOI]

Games, 2018

On relative and probabilistic finite counterability.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2018

Spanning the spectrum from safety to liveness.

[BibT_eX]

[DOI]

Acta Informatica, 2018

Spanning-Tree Games.

[BibT_eX]

[DOI]

Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science, 2018

Timed Network Games with Clocks.

[BibT_eX]

[DOI]

Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science, 2018

Alternating Reachability Games with Behavioral and Revenue Objectives.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Playing with the Maximum-Flow Problem.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Synthesis of Controllable Nash Equilibria in Quantitative Objective Game.

[BibT_eX]

[DOI]

Giuseppe Perelli

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

The Unfortunate-Flow Problem.

[BibT_eX]

[DOI]

Proceedings of the 45th International Colloquium on Automata, Languages, and Programming, 2018

Timed Vacuity.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017

Latticed-LTL synthesis in the presence of noisy inputs.

[BibT_eX]

[DOI]

Discret. Event Dyn. Syst., 2017

Hierarchical Network Formation Games.

[BibT_eX]

[DOI]

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

Examining classical graph-theory problems from the viewpoint of formal-verification methods (invited talk).

[BibT_eX]

[DOI]

Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, 2017

An Abstraction-Refinement Methodology for Reasoning about Network Games.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

Flow Games.

[BibT_eX]

[DOI]

Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2017

How Deterministic are Good-For-Games Automata?.

[BibT_eX]

[DOI]

Michal Skrzypczak

Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2017

Quantitative Assume Guarantee Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

Formally Reasoning About Quality.

[BibT_eX]

[DOI]

J. ACM, 2016

Network-formation games with regular objectives.

[BibT_eX]

[DOI]

Inf. Comput., 2016

Synthesis with rational environments.

[BibT_eX]

[DOI]

Giuseppe Perelli

Ann. Math. Artif. Intell., 2016

Eulerian Paths with Regular Constraints.

[BibT_eX]

[DOI]

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

On the Capacity of Capacitated Automata.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2016

On High-Quality Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2016

High-Quality Synthesis Against Stochastic Environments.

[BibT_eX]

[DOI]

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis.

[BibT_eX]

[DOI]

Yaron Velner

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

2015

Minimizing Deterministic Lattice Automata.

[BibT_eX]

[DOI]

Shulamit Halamish

ACM Trans. Comput. Log., 2015

Prime languages.

[BibT_eX]

[DOI]

Jonathan Mosheiff

Inf. Comput., 2015

Stochastization of Weighted Automata.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2015, 2015

Congestion Games with Multisets of Resources and Applications in Synthesis.

[BibT_eX]

[DOI]

Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

The Sensing Cost of Monitoring and Synthesis.

[BibT_eX]

[DOI]

Denis Kuperberg

Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

Repairing Multi-Player Games.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Concurrency Theory, 2015

Inherent Vacuity in Lattice Automata.

[BibT_eX]

[DOI]

Hila Gonen

Proceedings of the Fields of Logic and Computation II, 2015

2014

Temporal Specifications with Accumulative Values.

[BibT_eX]

[DOI]

Krishnendu Chatterjee

ACM Trans. Comput. Log., 2014

Parameterized Weighted Containment.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2014

An abstraction-refinement framework for trigger querying.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

Variations on Safety.

[BibT_eX]

[DOI]

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

Discounting in LTL.

[BibT_eX]

[DOI]

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

Properties and Utilization of Capacitated Automata (Invited Talk).

[BibT_eX]

[DOI]

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

Regular Sensing.

[BibT_eX]

[DOI]

Denis Kuperberg

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

From Reachability to Temporal Specifications in Cost-Sharing Games.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

A Game-Theoretic Approach to Simulation of Data-Parameterized Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

Rigorous approximated determinization of weighted automata.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2013

When does abstraction help?

[BibT_eX]

[DOI]

Inf. Process. Lett., 2013

Unifying Büchi Complementation Constructions

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2013

Profile Trees for Büchi Word Automata, with Application to Determinization.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fourth International Symposium on Games, 2013

Nondeterminism in the Presence of a Diverse or Unknown Future.

[BibT_eX]

[DOI]

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

Formalizing and Reasoning about Quality.

[BibT_eX]

[DOI]

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

Attention-Based Coverage Metrics.

[BibT_eX]

[DOI]

Shoham Ben-David

Proceedings of the Hardware and Software: Verification and Testing, 2013

Automatic Generation of Quality Specifications.

[BibT_eX]

[DOI]

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

Weighted Safety.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

A Framework for Ranking Vacuity Results.

[BibT_eX]

[DOI]

Shoham Ben-David

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

Translating to Co-Büchi Made Tight, Unified, and Useful.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2012

Once and for all.

[BibT_eX]

[DOI]

Amir Pnueli

J. Comput. Syst. Sci., 2012

Coping with selfish on-going behaviors.

[BibT_eX]

[DOI]

Inf. Comput., 2012

Improved model checking of hierarchical systems.

[BibT_eX]

[DOI]

Aniello Murano

Inf. Comput., 2012

Recent Challenges and Ideas in Temporal Synthesis.

[BibT_eX]

[DOI]

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

Environment-Friendly Safety.

[BibT_eX]

[DOI]

Sigal Weiner

Proceedings of the Hardware and Software: Verification and Testing, 2012

Making Weighted Containment Feasible: A Heuristic Based on Simulation and Abstraction.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

Approximating Deterministic Lattice Automata.

[BibT_eX]

[DOI]

Shulamit Halamish

Proceedings of the Automated Technology for Verification and Analysis, 2012

Model Checking Systems and Specifications with Parameterized Atomic Propositions.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2012

2011

Temporal Synthesis for Bounded Systems and Environments.

[BibT_eX]

[DOI]

Proceedings of the 28th International Symposium on Theoretical Aspects of Computer Science, 2011

Synthesis with Clairvoyance.

[BibT_eX]

[DOI]

Dorsa Sadigh

Sanjit A. Seshia

Proceedings of the Hardware and Software: Verification and Testing, 2011

Co-Büching Them All.

[BibT_eX]

[DOI]

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

Formal Analysis of Online Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2011

Max and Sum Semantics for Alternating Weighted Automata.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2011

2010

Multi-Valued Automata and Their Applications.

[BibT_eX]

[DOI]

Proceedings of the Logics and Languages for Reliability and Security, 2010

Erratum for "What causes a system to satisfy a specification?".

[BibT_eX]

[DOI]

Joseph Y. Halpern

ACM Trans. Comput. Log., 2010

Reasoning about online algorithms with weighted automata.

[BibT_eX]

[DOI]

ACM Trans. Algorithms, 2010

Latticed Simulation Relations and Games.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2010

Rational Synthesis.

[BibT_eX]

[DOI]

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

The Blowup in Translating LTL to Deterministic Automata.

[BibT_eX]

[DOI]

Adin Rosenberg

Proceedings of the Model Checking and Artificial Intelligence - 6th International Workshop, 2010

Synthesis of Trigger Properties.

[BibT_eX]

[DOI]

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

Variable Automata over Infinite Alphabets.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2010

Alternation Removal in Büchi Automata.

[BibT_eX]

[DOI]

Adin Rosenberg

Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010

Parityizing Rabin and Streett.

[BibT_eX]

[DOI]

Avital Steinitz

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

An Automata-Theoretic Approach to Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Time for Verification, 2010

The Quest for a Tight Translation of Büchi to co-Büchi Automata.

[BibT_eX]

[DOI]

Proceedings of the Fields of Logic and Computation, 2010

Promptness in omega-Regular Automata.

[BibT_eX]

[DOI]

Yoram Hirshfeld

Proceedings of the Automated Technology for Verification and Analysis, 2010

2009

From liveness to promptness.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2009

Co-ing Büchi Made Tight and Useful.

[BibT_eX]

[DOI]

Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

Reasoning about Finite-State Switched Systems.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2009

Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata.

[BibT_eX]

[DOI]

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

09501 Abstracts Collection - Software Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Software Synthesis, 06.12. - 11.12.2009, 2009

2008

What causes a system to satisfy a specification?.

[BibT_eX]

[DOI]

Joseph Y. Halpern

ACM Trans. Comput. Log., 2008

Multi-valued Logics, Automata, Simulations, and Games.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2008

Vacuity in Testing.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 2nd International Conference, 2008

On Verifying Fault Tolerance of Distributed Protocols.

[BibT_eX]

[DOI]

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

On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Word Automata.

[BibT_eX]

[DOI]

Omer Lev

Proceedings of the Logic for Programming, 2008

A Framework for Inherent Vacuity.

[BibT_eX]

[DOI]

Sarai Sheinvald-Faragy

Proceedings of the Hardware and Software: Verification and Testing, 2008

A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance.

[BibT_eX]

[DOI]

Wenchao Li

Sanjit A. Seshia

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

2007

Concurrent reachability games.

[BibT_eX]

[DOI]

Luca de Alfaro

Theor. Comput. Sci., 2007

Exponential Gaps in our Knowledge.

[BibT_eX]

Bull. EATCS, 2007

Lattice Automata.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2007

Better Under-Approximation of Programs by Hiding Variables.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2007

What Triggers a Behavior?

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Tightening the Exchange Rates Between Automata.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

Leaping Loops in the Presence of Abstraction.

[BibT_eX]

[DOI]

Mooly Sagiv

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

2006

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

[BibT_eX]

[DOI]

Rupak Majumdar

Theor. Comput. Sci., 2006

Coverage metrics for formal verification.

[BibT_eX]

[DOI]

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

Typeness for omega-regular Automata.

[BibT_eX]

[DOI]

Gila Morgenstern

Aniello Murano

Int. J. Found. Comput. Sci., 2006

Büchi Complementation Made Tighter.

[BibT_eX]

[DOI]

Ehud Friedgut

Int. J. Found. Comput. Sci., 2006

Coverage metrics for temporal logic model checking*.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2006

Relating word and tree automata.

[BibT_eX]

[DOI]

Shmuel Safra

Ann. Pure Appl. Log., 2006

On Locally Checkable Properties.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

Memoryful Branching-Time Logic.

[BibT_eX]

[DOI]

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Avoiding Determinization.

[BibT_eX]

[DOI]

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

An Abstraction-Refinement Framework for Multi-Agent Systems.

[BibT_eX]

[DOI]

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words.

[BibT_eX]

[DOI]

Sarai Sheinvald-Faragy

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

Sanity Checks in Formal Verification.

[BibT_eX]

[DOI]

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

Safraless Compositional Synthesis.

[BibT_eX]

[DOI]

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

On the Construction of Fine Automata for Safety Properties.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2006

On the Succinctness of Nondeterminism.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2006

2005

From linear time to branching time.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2005

From complementation to certification.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Complementation Constructions for Nondeterministic Automata on Infinite Words.

[BibT_eX]

[DOI]

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

Safraless Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 2005

Verifying Quantitative Properties Using Bound Functions.

[BibT_eX]

[DOI]

Arindam Chakrabarti

Krishnendu Chatterjee

Rupak Majumdar

Proceedings of the Correct Hardware Design and Verification Methods, 2005

Regular Vacuity.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2005

Abstraction for Falsification.

[BibT_eX]

[DOI]

Greta Yorsh

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

2004

w-Regular languages are testable with a constant number of queries.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2004

A Measured Collapse of the Modal µ-Calculus Alternation Hierarchy.

[BibT_eX]

[DOI]

Doron Bustan

Proceedings of the STACS 2004, 2004

Reasoning About Systems with Transition Fairness.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

2003

Response to "Comments on 'On Object Systems and Behavior Inheritance'".

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2003

Vacuity detection in temporal model checking.

[BibT_eX]

[DOI]

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

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

[BibT_eX]

[DOI]

Shaz Qadeer

Formal Methods Syst. Des., 2003

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

[BibT_eX]

[DOI]

Rupak Majumdar

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

Resets vs. Aborts in Linear Temporal Logic.

[BibT_eX]

[DOI]

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

Π2 ∩ Σ2 ≡ AFMC.

[BibT_eX]

[DOI]

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

On Complementing Nondeterministic Büchi Automata.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2003

Fair Equivalence Relations.

[BibT_eX]

[DOI]

Proceedings of the Verification: Theory and Practice, 2003

Formal Analysis of Scientific-Computation Methods.

[BibT_eX]

[DOI]

Gadiel Auerbach

Proceedings of the IFAC Conference on Analysis and Design of Hybrid Systems, 2003

2002

On Object Systems and Behavioral Inheritance.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2002

Alternating-time temporal logic.

[BibT_eX]

[DOI]

Rajeev Alur

J. ACM, 2002

Fair Simulation.

[BibT_eX]

[DOI]

Sriram K. Rajamani

Inf. Comput., 2002

On the Complexity of Verifying Concurrent Transition Systems.

[BibT_eX]

[DOI]

Inf. Comput., 2002

omega-Regular Languages Are Testable with a Constant Number of Queries.

[BibT_eX]

[DOI]

Proceedings of the Randomization and Approximation Techniques, 6th International Workshop, 2002

An Improved Algorithm for the Membership Problem for Extended Regular Expressions.

[BibT_eX]

[DOI]

Sharon Zuhovitzky

Proceedings of the Mathematical Foundations of Computer Science 2002, 2002

Pushdown Specifications.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2002

Coverage of Implementations by Simulating Specifications.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Information Technology in the Era of Networking and Mobile Computing, 2002

Synthesis of Uninitialized Systems.

[BibT_eX]

[DOI]

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

Trading Probability for Fairness.

[BibT_eX]

[DOI]

Marcin Jurdzinski

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

Model Checking Linear Properties of Prefix-Recognizable Systems.

[BibT_eX]

[DOI]

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

The Complexity of the Graded µ-Calculus.

[BibT_eX]

[DOI]

Ulrike Sattler

Proceedings of the Automated Deduction, 2002

2001

Weak alternating automata are not that weak.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2001

Module Checking.

[BibT_eX]

[DOI]

Pierre Wolper

Inf. Comput., 2001

Model Checking of Safety Properties.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

Coverage Metrics for Temporal Logic Model Checking.

[BibT_eX]

[DOI]

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

On Bounded Specifications.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2001

Synthesizing Distributed Systems.

[BibT_eX]

[DOI]

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

On the Complexity of Parity Word Automata.

[BibT_eX]

[DOI]

Valerie King

Proceedings of the Foundations of Software Science and Computation Structures, 2001

Extended Temporal Logic Revisited.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2001, 2001

A Practical Approach to Coverage in Model Checking.

[BibT_eX]

[DOI]

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

2000

An automata-theortetic approach to modular model checking.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2000

An automata-theoretic approach to branching-time model checking.

[BibT_eX]

[DOI]

Pierre Wolper

J. ACM, 2000

Branching-Depth Hierarchies.

[BibT_eX]

[DOI]

Shoham Shamir

Eli Shamir

Proceedings of the 7th International Workshop on Expressiveness in Concurrency, 2000

On the Behavioral Inheritance of State-Based Objects.

[BibT_eX]

[DOI]

Proceedings of the TOOLS 2000: 34th International Conference on Technology of Object-Oriented Languages and Systems, 30 July, 2000

µ-Calculus Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

Open Systems in Reactive Environments: Control and Synthesis.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2000, 2000

An Automata-Theoretic Approach to Reasoning about Infinite-State Systems.

[BibT_eX]

[DOI]

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

1999

Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions.

[BibT_eX]

[DOI]

J. Log. Comput., 1999

Church's problem revisited.

[BibT_eX]

[DOI]

Bull. Symb. Log., 1999

The Weakness of Self-Complementation.

[BibT_eX]

[DOI]

Proceedings of the STACS 99, 1999

Robust Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '99: Concurrency Theory, 1999

1998

Verification of Fair Transition Systems.

[BibT_eX]

[DOI]

Chic. J. Theor. Comput. Sci., 1998

Weak Alternating Automata and Tree Automata Emptiness.

[BibT_eX]

[DOI]

Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, 1998

Relating linear and branching model checking.

[BibT_eX]

Proceedings of the Programming Concepts and Methods, 1998

Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

Alternating Refinement Relations.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '98: Concurrency Theory, 1998

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

[BibT_eX]

[DOI]

Shaz Qadeer

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

1997

From Quantity to Quality.

[BibT_eX]

[DOI]

Proceedings of the Hybrid and Real-Time Systems, 1997

Existence of Reduction Hierarchies.

[BibT_eX]

[DOI]

Robert P. Kurshan

Mihalis Yannakakis

Proceedings of the Computer Science Logic, 11th International Workshop, 1997

Modular Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

Module Checking Revisited.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996

Buy One, Get One Free!!!

[BibT_eX]

[DOI]

J. Log. Comput., 1996

Branching-Time Temporal Logic and Tree Automata.

[BibT_eX]

[DOI]

Inf. Comput., 1996

Not checking for closure under stuttering.

[BibT_eX]

[DOI]

Gerard J. Holzmann

Proceedings of the Spin Verification System, 1996

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

[BibT_eX]

[DOI]

Proceedings of the CONCUR '96, 1996

Verification of Fair Transisiton Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Module Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995

Model checking for Branching-Time temporal logics.

[BibT_eX]

[DOI]

PhD thesis, 1995

Once and For All

[BibT_eX]

[DOI]

Amir Pnueli

Proceedings of the Proceedings, 1995

On the Complexity of Branching Modular Model Checking (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the CONCUR '95: Concurrency Theory, 1995

1994

An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract).

[BibT_eX]

[DOI]

Orna Bernholtz

Pierre Wolper

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

1993

Branching Time Temporal Logic and Amorphous Tree Automata.

[BibT_eX]

[DOI]

Orna Bernholtz