Ranking Function Synthesis for Bit-Vector Relations

DOI10.1007/978-3-642-12002-2_19zbMath1284.68172OpenAlexW2161217905MaRDI QIDQ3557080

Byron Cook, Christoph M. Wintersteiger, Daniel Kroening, Philipp Rümmer

Publication date: 27 April 2010

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-12002-2_19

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (11)

Efficiently solving quantified bit-vector formulas ⋮ Loop Summarization and Termination Analysis ⋮ Counterexample-Guided Model Synthesis ⋮ Complexity of fixed-size bit-vector logics ⋮ Loop summarization using state and transition invariants ⋮ Ranking function synthesis for bit-vector relations ⋮ Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development ⋮ Transfer Function Synthesis without Quantifier Elimination ⋮ Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers ⋮ Incremental Determinization ⋮ Ranking Functions for Linear-Constraint Loops

Uses Software

• QuBE++
• ARMC

This page was built for publication: Ranking Function Synthesis for Bit-Vector Relations