Ranking function synthesis for bit-vector relations

DOI10.1007/S10703-013-0186-4MaRDI QIDQ2248069zbMATH OpenOpenAlexFDO

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

Publication date 30 June 2014

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-013-0186-4

zbMATH Keywords

bit-vectorsranking functionssoftware verificationtermination

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Ranking function synthesis for bit-vector relations
• A new look at the automatic synthesis of linear ranking functions
• scientific article; zbMATH DE number 1701751
• Computer Aided Verification
• scientific article; zbMATH DE number 1903370

Cites work

• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• A First Step Towards a Unified Proof Checker for QBF
• Automated Deduction – CADE-20
• Automatic verification of counter systems with ranking function
• Compressing BMC encodings with QBF
• CONCUR 2005 – Concurrency Theory
• Efficiently solving quantified bit-vector formulas
• Formal Methods in Computer-Aided Design
• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 3560737 (Why is no real title available?)
• Leaping Loops in the Presence of Abstraction
• Predicate abstraction of ANSI-C programs using SAT
• Ranking function synthesis for bit-vector relations
• Scalable Shape Analysis for Systems Code
• Software verification for weak memory via program transformation
• Static Analysis
• Theory and Applications of Satisfiability Testing
• Verification, Model Checking, and Abstract Interpretation

Cited in

(9)

• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• On the complexity of the quantified bit-vector arithmetic with binary encoding
• Synthesizing ranking functions for loop programs via SVM
• Explaining AI decisions using efficient methods for learning sparse Boolean formulae
• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• Ranking function synthesis for bit-vector relations
• Proving termination of programs with bitvector arithmetic by symbolic execution
• Transfer function synthesis without quantifier elimination
• Truncating abstraction of bit-vector operations for BDD-based SMT solvers

Describes a project that uses

Uses Software

• QUBE
• QuBE++
• sKizzo
• ARMC
• bv2epr
• Quantor

This page was built for publication: Ranking function synthesis for bit-vector relations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2248069)