Ranking function synthesis for bit-vector relations
From MaRDI portal
Publication:2248069
DOI10.1007/s10703-013-0186-4zbMath1291.68138OpenAlexW2071969326MaRDI QIDQ2248069
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
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (4)
Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution ⋮ Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution ⋮ On the complexity of the quantified bit-vector arithmetic with binary encoding ⋮ Explaining AI decisions using efficient methods for learning sparse Boolean formulae
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Predicate abstraction of ANSI-C programs using SAT
- Efficiently solving quantified bit-vector formulas
- Compressing BMC Encodings with QBF
- Scalable Shape Analysis for Systems Code
- Ranking Function Synthesis for Bit-Vector Relations
- A First Step Towards a Unified Proof Checker for QBF
- Automatic Verification of Counter Systems With Ranking Function
- Software Verification for Weak Memory via Program Transformation
- Automated Deduction – CADE-20
- Leaping Loops in the Presence of Abstraction
- Formal Methods in Computer-Aided Design
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Theory and Applications of Satisfiability Testing
- Static Analysis
- CONCUR 2005 – Concurrency Theory
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Ranking function synthesis for bit-vector relations
