Challenges in Constraint-Based Analysis of Hybrid Systems

DOI10.1007/978-3-642-03251-6_4zbMath1248.68328OpenAlexW1509735216MaRDI QIDQ5191406

Natalia Kalinnik, Andreas Eggers, Tino Teige, Stefan Kupferschmid

Publication date: 6 August 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03251-6_4

zbMATH Keywords

differential equationsCraig interpolationparallel solvermixed Boolean and arithmetic constraintsstochastic SMT

Mathematics Subject Classification ID

Related Items (1)

Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties

Uses Software

• HySAT
• PSATO
• BLAST
• SATO
• MathSAT
• FOCI
• ABsolver
• PaMira
• PaSAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• Games against nature
• Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
• A fast parallel SAT-solver -- efficient workload balancing
• Accelerating bounded model checking of safety properties
• PSATO: A distributed propositional prover and its application to quasigroup problems
• An interpolating theorem prover
• Parallel SAT Solving in Bounded Model Checking
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems
• SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Hybrid Systems: Computation and Control
• Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic
• Constraint Solving for Interpolation
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Computer Aided Verification

This page was built for publication: Challenges in Constraint-Based Analysis of Hybrid Systems