A Library Modeling Language for the Static Analysis of C Programs
summary
Language for writing library stubs as logic formulas that model non-deterministic side effects (allocations, assigns with primed output variables) and resources (File class) and whose concrete semantics are defined by abstract interpretation. Implemented in the Mopsa framework with an extensible AST and domains like StringLength, PointerBaseOffset, polyhedra and recency, plus generic iterator and quantified-formula domains. Over 1,000 GNU libc functions modeled; Juliet benchmarks and 19 Coreutils programs run — many cases precise, integer-overflow tests show imprecision, analyses finish in minutes.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:16Problem Statement
- 1:07Running Example: mini-wc
- 1:48Concrete Semantics By Example: fopen
- 3:03How does alloc work?
- 4:11Concrete Semantics by Example: Igets
- 5:04How does assigns work?
- 6:01Abstraction Architecture
- 7:56Generic Stub Domains
- 9:30Example Configuration
- 10:54Abstraction of Relations
- 12:06How To Evaluate Quantified Formulas Efficiently?
- 15:16Benchmarks: Juliet
- 16:43Benchmarks: GNU Coreutils
- 18:03Conclusion
related talks
23mTargeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code
14mLexy: A DSL Library For C++ Parsing
19mA Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code
59mMeta++: Language Support for Advanced Generative Programming
01h 35mWriting a Base Level Library for Safety Critical Code in C++
01h 08mC++ Metaprogramming: A Paradigm Shift
01h 16m2024 Update: Efficient and Reliable Wrapping of C APIs Using Modern C++
20mMisconceptions About Loops in C