Orna Grumberg

Affiliations:
  • Technion - Israel Institute of Technology, Haifa, Israel


According to our database1, Orna Grumberg authored at least 137 papers between 1983 and 2023.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 2015, "For contributions to research in automated formal verification of hardware and software systems.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Condition Synthesis Realizability via Constrained Horn Clauses.
Proceedings of the NASA Formal Methods - 15th International Symposium, 2023

Structure-Guided Solution of Constrained Horn Clauses.
Proceedings of the Automated Technology for Verification and Analysis, 2023

2022
Assume, guarantee or repair: a regular framework for non regular properties.
Int. J. Softw. Tools Technol. Transf., 2022

Edmund Melson Clarke, Jr. (1945-2020).
Formal Methods Syst. Des., 2022

Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties (full version).
CoRR, 2022

Automated Program Repair Using Formal Verification Techniques.
Proceedings of the Principles of Systems Design, 2022

2021
Compositional Model Checking for Multi-properties.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

2020
Assume, Guarantee or Repair.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Must Fault Localization for Program Repair.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains.
J. Autom. Reason., 2019

Topology-Agnostic Runtime Detection of OSPF Routing Attacks.
Proceedings of the 7th IEEE Conference on Communications and Network Security, 2019

2018
Abstraction and Abstraction Refinement.
Proceedings of the Handbook of Model Checking., 2018

Automated circular assume-guarantee reasoning.
Formal Aspects Comput., 2018

Program repair that learns from mistakes.
Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, 2018

Modular Verification of Concurrent Programs via Sequential Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2018

Model checking, 2nd Edition.
MIT Press, ISBN: 978-0-262-03883-6, 2018

2017
Formal Black-Box Analysis of Routing Protocol Implementations.
CoRR, 2017

Modular Demand-Driven Analysis of Semantic Difference for Program Versions.
Proceedings of the Static Analysis - 24th International Symposium, 2017

An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data.
Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

2016
Learning-Based Compositional Model Checking of Behavioral UML Systems.
Proceedings of the Dependable Software Systems Engineering, 2016

A framework for compositional verification of multi-valued systems via abstraction-refinement.
Inf. Comput., 2016

Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201).
Dagstuhl Reports, 2016

Sound and Complete Mutation-Based Program Repair.
Proceedings of the FM 2016: Formal Methods, 2016

Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015
Analyzing Internet Routing Security Using Model Checking.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Learning-Based Compositional Model Checking of Behavioral UML Systems.
Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

2014
SAT-based Model Checking: Interpolation, IC3, and Beyond.
Proceedings of the Software Systems Safety, 2014

Verifying Behavioral UML Systems via CEGAR.
Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

A Game-Theoretic Approach to Simulation of Data-Parameterized Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2014

2013
Intertwined Forward-Backward Reachability Analysis Using Interpolants.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
Model Checking: From BDDs to Interpolation.
Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012

Multi-valued model checking games.
J. Comput. Syst. Sci., 2012

2010 CAV award announcement.
Formal Methods Syst. Des., 2012

Lazy abstraction and SAT-based reachability in hardware model checking.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

Applying Software Model Checking Techniques for Behavioral UML Models.
Proceedings of the FM 2012: Formal Methods, 2012

Model Checking Systems and Specifications with Parameterized Atomic Propositions.
Proceedings of the Automated Technology for Verification and Analysis, 2012

2010
2-Valued and 3-Valued Abstraction-Refinement in Model Checking.
Proceedings of the Logics and Languages for Reliability and Security, 2010

Compositional verification and 3-valued abstractions join forces.
Inf. Comput., 2010

2009 CAV award announcement.
Formal Methods Syst. Des., 2010

Variable Automata over Infinite Alphabets.
Proceedings of the Language and Automata Theory and Applications, 2010

2009
Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification.
Int. J. Softw. Tools Technol. Transf., 2009

Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations.
Formal Methods Syst. Des., 2009

The 2008 CAV Award citation.
Formal Methods Syst. Des., 2009

Interpolation-sequence based model checking.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Hybrid BDD and All-SAT Method for Model Checking.
Proceedings of the Languages: From Formal to Natural, 2009

3-Valued Abstraction for (Bounded) Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2009

2008
3-Valued abstraction: More precision at less cost.
Inf. Comput., 2008

Efficient Automatic STE Refinement Using Responsibility.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

2007
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
ACM Trans. Comput. Log., 2007

VeriTech: a framework for translating among model description notations.
Int. J. Softw. Tools Technol. Transf., 2007

Verifying Very Large Industrial Circuits Using 100 Processes and Beyond.
Int. J. Found. Comput. Sci., 2007

When not losing is better than winning: Abstraction and refinement for the full mu-calculus.
Inf. Comput., 2007

A New Approach to Bounded Model Checking for Branching Time Logics.
Proceedings of the Automated Technology for Verification and Analysis, 2007

3-Valued Circuit SAT for STE with Automatic Refinement.
Proceedings of the Automated Technology for Verification and Analysis, 2007

2006
A work-efficient distributed algorithm for reachability analysis.
Formal Methods Syst. Des., 2006

Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

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

Distributed Symbolic Model Checking for µ-Calculus.
Formal Methods Syst. Des., 2005

Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking.
Formal Methods Syst. Des., 2005

<i>Don't Know</i> in the µ-Calculus.
Proceedings of the Verification, 2005

Proof-guided underapproximation-widening for multi-process systems.
Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

State/Event Software Verification for Branching-Time Specifications.
Proceedings of the Integrated Formal Methods, 5th International Conference, 2005

Abstraction and Refinement in Model Checking.
Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation.
Proceedings of the Correct Hardware Design and Verification Methods, 2005

Regular Vacuity.
Proceedings of the Correct Hardware Design and Verification Methods, 2005

Bounded Model Checking of Concurrent Programs.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
Test sequence generation and model checking using dynamic transition relations.
Int. J. Softw. Tools Technol. Transf., 2004

Applicability of fair simulation.
Inf. Comput., 2004

Static Analysis for State-Space Reductions Preserving Temporal Logics.
Formal Methods Syst. Des., 2004

Monotonic Abstraction-Refinement for CTL.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis.
Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

2003
Simulation-based minimazation.
ACM Trans. Comput. Log., 2003

Scalable distributed on-the-fly symbolic model checking.
Int. J. Softw. Tools Technol. Transf., 2003

Learning to Order BDD Variables in Verification.
J. Artif. Intell. Res., 2003

Counterexample-guided abstraction refinement for symbolic model checking.
J. ACM, 2003

Preface.
Proceedings of the 2nd International Workshop on Parallel and Distributed Model Checking, 2003

High Level Verification of Control Intensive Systems Using Predicate Abstraction.
Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Enhanced Vacuity Detection in Linear Temporal Logic.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
Syntax-directed model checking of sequential programs.
J. Log. Algebraic Methods Program., 2002

A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits.
Formal Methods Syst. Des., 2002

Different directions in parallel and distributed model checking (invited talk).
Proceedings of the Parallel and Distributed Model Checking, 2002

Translations between Textual Transition Systems and Petri Nets.
Proceedings of the Integrated Formal Methods, Third International Conference, 2002

A Framework for Translating Models and Specifications.
Proceedings of the Integrated Formal Methods, Third International Conference, 2002

2001
Which Branching-Time Properties are Effectively Linear?
J. Log. Comput., 2001

Introduction: Special Issue on CAV '97.
Formal Methods Syst. Des., 2001

Progress on the State Explosion Problem in Model Checking.
Proceedings of the Informatics - 10 Years Back. 10 Years Ahead., 2001

Model checking, 1st Edition.
MIT Press, ISBN: 978-0-262-03270-4, 2001

2000
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System.
Formal Methods Syst. Des., 2000

Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Counterexample-Guided Abstraction Refinement.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Simulation Based Minimization.
Proceedings of the Automated Deduction, 2000

1999
State Space Reduction Using Partial Order Techniques.
Int. J. Softw. Tools Technol. Transf., 1999

Preface.
Proceedings of the First International Workshop on Symbolic Model Checking, 1999

"Have I written enough Properties?" - A Method of Comparison between Specification and Implementation.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998
Modular Model Checking of Software.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

First-Order-CTL Model Checking.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1998

1997
Abstract Interpretation of Reactive Systems.
ACM Trans. Program. Lang. Syst., 1997

Verifying Parameterized Networks.
ACM Trans. Program. Lang. Syst., 1997

Another Look at LTL Model Checking.
Formal Methods Syst. Des., 1997

1996
Buy One, Get One Free!!!
J. Log. Comput., 1996

Verification of Temporal Properties.
J. Log. Comput., 1996

Branching-Time Temporal Logic and Tree Automata.
Inf. Comput., 1996

Model checking.
Proceedings of the NATO Advanced Study Institute on Deductive Program Design, 1996

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995
Verification of the Futurebus+ Cache Coherence Protocol.
Formal Methods Syst. Des., 1995

Efficient On-the-Fly Model Checking for CTL*
Proceedings of the Proceedings, 1995

Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.
Proceedings of the 32st Conference on Design Automation, 1995

Veryfying Parameterized Networks using Abstraction and Regular Languages.
Proceedings of the CONCUR '95: Concurrency Theory, 1995

What if model checking must be truly symbolic.
Proceedings of the Correct Hardware Design and Verification Methods, 1995

1994
Model Checking and Modular Verification.
ACM Trans. Program. Lang. Syst., 1994

Model Checking and Abstraction.
ACM Trans. Program. Lang. Syst., 1994

Program Composition via Unification.
Theor. Comput. Sci., 1994

How Linear Can Branching-Time Be?
Proceedings of the Temporal Logic, First International Conference, 1994

1993
Modular Abstractions for Verifying Real-Time Distributed Systems.
Formal Methods Syst. Des., 1993

Fairness and Hyperfairness in Multi-Party Interactions.
Distributed Comput., 1993

Verification Tools for Finite-State Concurrent Systems.
Proceedings of the A Decade of Concurrency, Reflections and Perspectives, 1993

Branching Time Temporal Logic and Amorphous Tree Automata.
Proceedings of the CONCUR '93, 1993

Generation of Reduced Models for Checking Fragments of CTL.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992
A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems.
J. Log. Comput., 1992

1991
Program Composition and Modular Verification.
Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991

1990
Sematics-Driven Decompositions for the Verification of Distributed Programs.
Proceedings of the Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 1990

The Modular Framework of Computer-Aided Verification.
Proceedings of the Computer Aided Verification, 2nd International Workshop, 1990

1989
Reasoning about Networks with Many Identical Finite State Processes
Inf. Comput., April, 1989

Network Grammars, Communication Behaviors and Automatic Verification.
Proceedings of the Automatic Verification Methods for Finite State Systems, 1989

1988
Infinite Trees, Markings and Well-Foundedness
Inf. Comput., November, 1988

Characterizing Finite Kripke Structures in Propositional Temporal Logic.
Theor. Comput. Sci., 1988

1987
The Model Checking Problem for Concurrent Systems with Many Similar Processes.
Proceedings of the Temporal Logic in Specification, 1987

Characterizing Kripke Structures in Temporal Logic.
Proceedings of the TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1987

Avoiding The State Explosion Problem in Temporal Logic Model Checking.
Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, 1987

1986
A Complete Rule for Equifair Termination.
J. Comput. Syst. Sci., 1986

1985
A Proof Rule for Fair Termination of Guarded Commands
Inf. Control., 1985

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

1984
Fail Termination of Communicating Processe.
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, 1984

1983
A Compete Proof Rule for Strong Equifair Termination.
Proceedings of the Logics of Programs, 1983


  Loading...