Abstract interpretation of microcontroller code: intervals meet congruences

DOI10.1016/j.scico.2012.06.001zbMath1284.68167OpenAlexW2125299071MaRDI QIDQ2442953

Jörg Brauer, Andy King, Stefan Kowalewski

Publication date: 2 April 2014

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2012.06.001

zbMATH Keywords

intervalsembedded systemsabstract interpretationbinary codelinear congruences

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Goanna
• Sat4j
• Java PathFinder
• BitBlaze
• BAP
• WPDS++
• Mjollnir

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Application of static analyses for state-space reduction to the microcontroller binary code
• The two variable per inequality abstract domain
• Why does Astrée scale up?
• A structure-preserving clause form translation
• Affine relationships among variables of a program
• Model checking JAVA programs using JAVA PathFinder
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Range and Set Abstraction using SAT
• Refinement-Based CFG Reconstruction from Unstructured Programs
• Lifting abstract interpreters to quantified logical domains
• Inferring Congruence Equations Using SAT
• Splitting the Control Flow with Boolean Flags
• Loop Summarization Using Abstract Transformers
• Automatic Modular Abstractions for Template Numerical Constraints
• Grids: A Domain for Analyzing the Distribution of Numerical Values
• An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries
• SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities
• Taming the Wrapping of Integer Arithmetic
• Automatic Abstraction for Congruences
• Static analysis of arithmetical congruences
• Automatic Abstraction for Intervals Using Boolean Formulae
• Automatic modular abstractions for linear constraints
• A framework for numeric analysis of array operations
• Programming Languages and Systems
• Programming Languages and Systems
• Leaping Loops in the Presence of Abstraction
• Logic programming with satisfiability
• Static Analysis
• Computer Aided Verification
• Transfer Function Synthesis without Quantifier Elimination
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Abstract interpretation of microcontroller code: intervals meet congruences