Optimality in Abstractions of Model Checking

No abstract is available for this paper.

• Publication year

  1995

• Venue

  Sensors Applications Symposium

• Publication date

  1995-09-25

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/3-540-60360-3_32
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Abstract interpretation of reactive systems : abstractions preserving $\forall$CTL*, $\exists$CTL* and CTL*

  1994influential reference
• Abstractions for Preserving All CTL* Formulae

  1994cited by this paper
• Automatic Veriication of Nite-state Concurrent Systems Using Temporal-logic Speciications. Acm

  1993cited by this paper
• Property Preserving Simulations

  1992cited by this paper
• Model checking and abstraction

  1992influential reference
• Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation

  1992cited by this paper
• Symbolic Model Checking with Partitioned Transistion Relations

  1991cited by this paper
• The Temporal Logic of Reactive and Concurrent Systems

  1991cited by this paper
• Modal Specifications

  1989cited by this paper
• Automatic verification of finite-state concurrent systems using temporal logic specifications

  1986cited by this paper
• “Sometimes” and “not never” revisited: on branching versus linear time temporal logic

  1986cited by this paper
• Specification and verification of concurrent systems in CESAR

  1982cited by this paper
• Systematic design of program analysis frameworks

  1979cited by this paper

• The role of model checking in software engineering

  2018cites this paper
• Inverse-limit and topological aspects of abstract interpretation

  2012cites this paper
• Finite-state abstractions for probabilistic computation tree logic

  2011cites this paper
• Abstract Interpretation from a Topological Perspective

  2009cites this paper
• Behavioural Model Fusion

  2008influential citation
• Improving software comprehension in regulating safety -critical systems

  2008cites this paper
• An Abstraction-Based Analysis of Rule Systems for Active Database Management Systems

  2007cites this paper
• More Precise Partition Abstractions

  2007cites this paper
• Extracting Program Logics From Abstract Interpretations Defined by Logical Relations

  2007cites this paper
• An Interval Framework for Process Algebras, Reenement, and Model Checking

  2007cites this paper
• ON THE EVOLUTION OF RELIABILITY METHODS FOR CRITICAL SOFTWARE

  2006cites this paper
• Underapproximating Predicate Transformers

  2006cites this paper
• State-rich model checking

  2006cites this paper
• 3-Valued Abstraction: More Precision at Less Cost

  2006cites this paper
• Thorough Checking Revisited

  2006cites this paper
• Comparing Completeness Properties of Static Analyses and Their Logics

  2006cites this paper
• Automata as Abstractions

  2005cites this paper
• Generalized Strong Preservation by Abstract Interpretation

  2004cites this paper
• Three-valued abstractions of games: uncertainty, but with precision

  2004cites this paper
• Refining Model Checking by Abstract Interpretation

  2004cites this paper
• Abstraction-Based Model Checking Using Heuristical Refinement

  2004cites this paper
• The existence of finite abstractions for branching time model checking

  2004cites this paper
• Scalable design of fault-tolerance for wireless sensor networks

  2004cites this paper
• αSPIN: A tool for abstract model checking

  2004cites this paper
• Hierarchical modeling and analysis of timed systems

  2003cites this paper
• From Trace Sets to Modal-Transition Systems by Stepwise Abstract Interpretation

  2003cites this paper
• Abstract model checking and refinement of temporal logic in /spl alpha/SPIN

  2003cites this paper
• Abstraction for Branching Time Properties

  2003cites this paper
• On Abstraction in Software Verification

  2002cites this paper
• Possibilistic and Probabilistic Abstraction-Based Model Checking

  2002cites this paper
• Static Analysis

  2002influential citation
• SAT-based counterexample-guided abstraction refinement

  2002cites this paper
• An Algebraic Framework for Abstract Model Checking

  2002cites this paper
• Refinement of LTL Formulas for Abstract Model Checking

  2002influential citation
• Abstraction-Based Model Checking Using Modal Transition Systems

  2001cites this paper
• Abstract Interpretation Based Formal Methods and Future Challenges

  2001cites this paper
• Boolean and Cartesian abstraction for model checking C programs

  2001cites this paper
• Model checking security properties of control flow graphs

  2001cites this paper
• Verification of Embedded Software: Problems and Perspectives

  2001cites this paper
• Incremental Verification by Abstraction

  2001cites this paper
• Temporal abstract interpretation

  2000cites this paper
• Making abstract interpretations complete

  2000cites this paper
• Binary Relations for Abstraction and Refinement

  2000influential citation
• Abstract interpretation based program testing

  2000cites this paper
• Interpretation Based Program Testing Patrick Cousot Département d ’ informatique École normale supérieure 45 rue d ’ Ulm 75230 Paris cedex 05 , France

  2000cites this paper
• System Description, Abstraction, and Veriication: a Uniform Treatment of Quality and Quantity

  1999cites this paper
• Using Abstract Interpretation for the Safe Verification of Security Protocols

  1999cites this paper
• Applications of Abstraction for Concurrent Programs

  1999cites this paper
• Verification of control flow based security properties

  1999cites this paper
• Trace-Based Abstract Interpretation of Operational Semantics

  1998cites this paper
• A symbolic semantics for abstract model checking

  1998cites this paper
• Abstract Games for Infinite State Processes

  1998cites this paper
• Program Analysis as Model Checking of Abstract Interpretations

  1998cites this paper
• Parallel combination of abstract interpretation and model-based automatic analysis of software

  1997cites this paper
• Towards a Mechanization of Cryptographic Protocal Verification

  1997cites this paper
• Abstract interpretation of reactive systems

  1997cites this paper
• Limiting State Explosion with Filter-Based Re nement

  1997cites this paper
• Implementing a Static Analyzer of ConcurrentPrograms : Problems and PerspectivesR

  1996cites this paper
• Abstract interpretation and partition refinement for model checking

  1996cites this paper
• Abstract Interpretation and Application to Interactive System Verification

  1996cites this paper
• Abstract Interpretation of Small-Step Semantics

  1996cites this paper
• Implementing a Static Analyzer of Concurrent Programs: Problems and Perspectives

  1996cites this paper
• Incremental Veri(cid:12)cation by Abstraction ?

  year unknowncites this paper