Concept

Hypostatic abstraction

Related publications (9)

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Springer2015

Fabrication-Aware Design with Performative Criteria

Yuliy Gennadievich Schwartzburg

Artists and architects often need to handle multiple constraints during design of physical constructions. We define a performative constraint as any constraint on design that is tied to the performance of the model--either during fabrication, construction, ...

EPFL2015

Accelerating Interpolants

Viktor Kuncak, Hossein Hojjat

We present Counterexample-Guided Accelerated Abstraction Refinement (CEGAAR), a new algorithm for verifying infinite-state transition systems. CEGAAR combines interpolation-based predicate discovery in counterexample guided predicate abstraction with accel ...

2012

A Verification Toolkit for Numerical Transition Systems

Viktor Kuncak, Hossein Hojjat

This paper presents a publicly available toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We pres ...

2012

Interpolation and Symbol Elimination

Laura Ildiko Kovacs

We prove several results related to local proofs, interpolation and superposition calculus and discuss their use in predicate abstraction and invariant generation. Our proofs and results suggest that symbol-eliminating inferences may be an interesting alte ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2009

Analysis and Design of Biological Circuits and Systems

Systems and synthetic biology are two emerging disciplines that hold promise to revolutionize our understanding of biological systems and to herald a new era of programmable hardware, respectively. Mathematical abstraction and today's abundance of quantita ...

IEEE2009

Program Analysis with Dynamic Precision Adjustment

Grégory Théoduloz, Dirk Thilo Beyer

We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a ...

IEEE2008

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

Grégory Théoduloz, Dirk Thilo Beyer

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this p ...

Springer2007

Lazy Shape Analysis

Grégory Théoduloz, Dirk Thilo Beyer

Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analy ...

Springer2006