MOPSA - Modular Open Platform for Static Analysis
  • 🏡 Home
  • ⚡ Features
  • 🔥 News
  • 👥 Team
  • 📚 Documentation
  • 💻 Code
  • 🎓 Publications
  • Get Started 🚀
Get Started 🚀
  • People
  • News
    • New Webpage
    • MOPSA 1.0 released!
    • Gold Medal 🥇 for the Software System category at SV-COMP 2024
  • Publications
    • Generation of violation witnesses by under-approximating abstract interpretation
    • Mopsa-C: Improved verification for C programs, simple validation of correctness witnesses (competition contribution)
    • Sound abstract nonexploitability analysis
    • Under-approximating memory abstractions
    • Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs
    • Mopsa-C: Modular domains and relational abstract interpretation for C programs (competition contribution)
    • Abstract interpretation of Michelson smart-contracts
    • Sound static analysis of regular expressions for vulnerabilities to denial of service attacks
    • Static analysis of program portability by abstract interpretation
    • A multilanguage static analysis of Python programs with native C extensions
    • Static analysis of endian portability by abstract interpretation
    • Static type and value analysis by abstract interpretation of Python programs with native C libraries
    • A library modeling language for the static analysis of C programs
    • Static type analysis by abstract interpretation of Python programs
    • Value and allocation sensitivity in static Python analyses
    • An abstract domain for trees with numeric relations
    • Analysis of program differences with numerical abstract interpretation
    • Analysis of software patches using numerical abstract interpretation
    • Combinations of reusable abstract domains for a multilingual static analyzer
    • Precise and modular static analysis by abstract interpretation for the automatic proof of program soundness and contracts inference
    • Quantitative static analysis of communication protocols using abstract Markov chains
    • Design of a modular platform for static analysis
    • Inferring functional properties of matrix manipulating programs by abstract interpretation
    • Modular static analysis of string manipulations in C programs
    • Static analysis by abstract interpretation collecting types of Python programs
    • Static value analysis of Python programs by abstract interpretation
    • Quantitative static analysis of communication protocols using abstract Markov chains
    • Tutorial on static inference of numeric invariants by abstract interpretation
    • Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs
  • Get Started!
Publications
Generation of violation witnesses by under-approximating abstract interpretation

Generation of violation witnesses by under-approximating abstract interpretation

Marco Milanese
Marco Milanese
Antoine Miné
Antoine Miné
PDF

MOPSA is an open-source project distributed under LGPL 3 licence.

Published with Hugo Blox Builder — the free, open source website builder that empowers creators.