Lattice-based refinement in bounded model checking (Q1629959)

From MaRDI portal

Jump to:navigation, search

scientific article

In more languages

Language	Label	Description	Also known as
English	Lattice-based refinement in bounded model checking	scientific article

Statements

scholarly article

Lattice-based refinement in bounded model checking (English)

Karine Even-Mendoza

Antti E. J. Hyvärinen

Natasha Sharygina

publication date

7 December 2018

MaRDI profile type

MaRDI publication profile

full work available at URL

https://doi.org/10.1007/978-3-030-03592-1_4

Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF

Satisfiability modulo transcendental functions via incremental linearization

Tools and Algorithms for the Construction and Analysis of Systems

Counterexample-guided abstraction refinement for symbolic model checking

Systematic design of program transformation frameworks by abstract interpretation

Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

Simplify: a theorem prover for program checking

Interpolant Strength

SMTCoq: a plug-in for integrating SMT solvers into Coq

Making abstract interpretations complete

Theory refinement for program verification

OpenSMT2: An SMT Solver for Multi-core and Cloud Computing

PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification

Identifiers

zbMATH Open document ID

10.1007/978-3-030-03592-1_4

Mathematics Subject Classification ID

zbMATH DE Number

Sitelinks

Mathematics(1 entry)

mardi Publication:1629959

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q1629959&oldid=36454820"