Application of static analyses for state-space reduction to the microcontroller binary code

DOI10.1016/j.scico.2010.03.006zbMath1213.68390OpenAlexW2139573796MaRDI QIDQ617924

Jörg Brauer, Bastian Schlich, Stefan Kowalewski

Publication date: 14 January 2011

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

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

zbMATH Keywords

model checkingstatic analysisabstractionbinary codeembedded software

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)

Related Items

Abstract interpretation of microcontroller code: intervals meet congruences

Uses Software

• StEAM
• Bandera
• Bebop
• GDB
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Properties of data flow frameworks: A unified model
• Static analysis for state-space reductions preserving temporal logics
• Inferring Congruence Equations Using SAT
• Automatic Abstraction for Congruences
• Branching time and abstraction in bisimulation semantics
• Stack-based typed assembly language
• Model Checking Software