Constraint-Based Abstraction of a Model Checker for Infinite State Systems

Gourinath Banda, John Patrick Gallagher

Publikation: KonferencebidragPaperForskningpeer review

Resumé

Abstract interpretation-based model checking provides an approach to verifying properties of infinite-state systems. In practice, most previous work on abstract model checking is either restricted to verifying universal properties, or develops special techniques for temporal logics such as modal transition systems or other dual transition systems. By contrast we apply completely standard techniques for constructing abstract interpretations to the abstraction of a CTL
semantic function, without restricting the kind of properties that can be verified. Furthermore we show that this leads directly to implementation of abstract model checking algorithms for abstract domains based on constraints, making use of an SMT solver.
OriginalsprogEngelsk
Publikationsdato2009
Antal sider16
StatusUdgivet - 2009
Begivenhed23rd Workshop on Constraint Logic Programming (WLP 2009) - Potsdam, Tyskland
Varighed: 15 sep. 200916 sep. 2009

Konference

Konference23rd Workshop on Constraint Logic Programming (WLP 2009)
LandTyskland
ByPotsdam
Periode15/09/200916/09/2009

Citer dette

Banda, G., & Gallagher, J. P. (2009). Constraint-Based Abstraction of a Model Checker for Infinite State Systems. Afhandling præsenteret på 23rd Workshop on Constraint Logic Programming (WLP 2009), Potsdam, Tyskland.
Banda, Gourinath ; Gallagher, John Patrick. / Constraint-Based Abstraction of a Model Checker for Infinite State Systems. Afhandling præsenteret på 23rd Workshop on Constraint Logic Programming (WLP 2009), Potsdam, Tyskland.16 s.
@conference{01be2090a8e811deb1a2000ea68e967b,
title = "Constraint-Based Abstraction of a Model Checker for Infinite State Systems",
abstract = "Abstract interpretation-based model checking provides an approach to verifying properties of infinite-state systems. In practice, most previous work on abstract model checking is either restricted to verifying universal properties, or develops special techniques for temporal logics such as modal transition systems or other dual transition systems. By contrast we apply completely standard techniques for constructing abstract interpretations to the abstraction of a CTL semantic function, without restricting the kind of properties that can be verified. Furthermore we show that this leads directly to implementation of abstract model checking algorithms for abstract domains based on constraints, making use of an SMT solver.",
keywords = "Model checking, Program analysis, Abstract Interpretation",
author = "Gourinath Banda and Gallagher, {John Patrick}",
year = "2009",
language = "English",
note = "null ; Conference date: 15-09-2009 Through 16-09-2009",

}

Banda, G & Gallagher, JP 2009, 'Constraint-Based Abstraction of a Model Checker for Infinite State Systems' Paper fremlagt ved 23rd Workshop on Constraint Logic Programming (WLP 2009), Potsdam, Tyskland, 15/09/2009 - 16/09/2009, .

Constraint-Based Abstraction of a Model Checker for Infinite State Systems. / Banda, Gourinath; Gallagher, John Patrick.

2009. Afhandling præsenteret på 23rd Workshop on Constraint Logic Programming (WLP 2009), Potsdam, Tyskland.

Publikation: KonferencebidragPaperForskningpeer review

TY - CONF

T1 - Constraint-Based Abstraction of a Model Checker for Infinite State Systems

AU - Banda, Gourinath

AU - Gallagher, John Patrick

PY - 2009

Y1 - 2009

N2 - Abstract interpretation-based model checking provides an approach to verifying properties of infinite-state systems. In practice, most previous work on abstract model checking is either restricted to verifying universal properties, or develops special techniques for temporal logics such as modal transition systems or other dual transition systems. By contrast we apply completely standard techniques for constructing abstract interpretations to the abstraction of a CTL semantic function, without restricting the kind of properties that can be verified. Furthermore we show that this leads directly to implementation of abstract model checking algorithms for abstract domains based on constraints, making use of an SMT solver.

AB - Abstract interpretation-based model checking provides an approach to verifying properties of infinite-state systems. In practice, most previous work on abstract model checking is either restricted to verifying universal properties, or develops special techniques for temporal logics such as modal transition systems or other dual transition systems. By contrast we apply completely standard techniques for constructing abstract interpretations to the abstraction of a CTL semantic function, without restricting the kind of properties that can be verified. Furthermore we show that this leads directly to implementation of abstract model checking algorithms for abstract domains based on constraints, making use of an SMT solver.

KW - Model checking

KW - Program analysis

KW - Abstract Interpretation

M3 - Paper

ER -

Banda G, Gallagher JP. Constraint-Based Abstraction of a Model Checker for Infinite State Systems. 2009. Afhandling præsenteret på 23rd Workshop on Constraint Logic Programming (WLP 2009), Potsdam, Tyskland.