HySAT: An efficient proof engine for bounded model checking of hybrid systems
type: Item
instance of: scholarly article
title: HySAT: An efficient proof engine for bounded model checking of hybrid systems
zbMATH Open document ID: 1116.68048
author: Martin Fränzle
author: Christian Herde
published in: Formal Methods in System Design
publication date: 2007-05-31T00:00:00Z
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5159783
zbMATH Keywords: Verification
zbMATH Keywords: Bounded model checking
zbMATH Keywords: Hybrid systems
zbMATH Keywords: Infinite-state systems
zbMATH Keywords: Decision procedures
zbMATH Keywords: Satisfiability
describes a project that uses: PBS
describes a project that uses: SATIRE
describes a project that uses: Chaff
describes a project that uses: MathSAT
MaRDI profile type: Publication
full work available at URL: s10703-006-0031-0
OpenAlex ID: W2086163366
cites work: Q4809056
cites work: Verifying industrial hybrid systems with \textsc{MathSAT}
cites work: Q4736486
cites work: Q4804899
cites work: Q4249562
cites work: Q4817533
cites work: Finding a Useful Subset of Constraints for Analysis in an Infeasible Linear Program
cites work: Locating Minimal Infeasible Constraint Sets in Linear Programs
cites work: A machine program for theorem-proving
cites work: Automated Reasoning
cites work: Q4809077
cites work: Q3408146
cites work: Identifying Minimally Infeasible Subsystems of Inequalities
cites work: Predicative programming Part I
cites work: Q4234084
cites work: An incremental algorithm to check satisfiability for bounded model checking
cites work: Q5760872
cites work: Computing small clause normal forms
cites work: Q3023951
cites work: Q2754108
cites work: A linear-time transformation of linear inequalities into conjunctive normal form
DOI: 10.1007/S10703-006-0031-0
description: scientific article; zbMATH DE number 5159783