Efficient Proof Engines for Bounded Model Checking of Hybrid Systems

Martin Fränzle; Christian Herde

doi:10.1016/j.entcs.2004.08.061

Efficient Proof Engines for Bounded Model Checking of Hybrid Systems

Authors:

Fränzle, Martin ;
Close
Department of Informatics and Mathematical Modeling, Technical University of Denmark
Herde, Christian
Close
unknown

DOI:

10.1016/j.entcs.2004.08.061

Abstract:

In this paper we present HySat, a new bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLL-based pseudo-Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits all of the various optimizations that arise naturally in the bounded model checking context, e.g. isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.

Type:

Journal article

Language:

English

Published in:

Electronic Notes in Theoretical Computer Science, 2005, Vol 133, p. 119-137

Keywords:

satisfiability; hybrid systems; infinite-state systems; verification; bounded model checking; decision procedures

Main Research Area:

Science/technology

Publication Status:

Published

Review type:

Peer Review

Submission year:

2005

Scientific Level:

Scientific

ID:

9205211

Efficient Proof Engines for Bounded Model Checking of Hybrid Systems

Full text access

On-site access

At institution

Example	Finds records
water{}	containing the word "water".
water supplies"{}"	containing the phrase "water supplies".
author:"Doe, John"author:"{}"	containing the prase "Doe, John" in the author field.
title:IEEEtitle:{}	containing the word "IEEE" in the title field.
Need more help?	Advanced search tutorial