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
Mopsa-C: Improved verification for C programs, simple validation of correctness witnesses (competition contribution)

Mopsa-C: Improved verification for C programs, simple validation of correctness witnesses (competition contribution)

Raphaël Monat
Raphaël Monat
Marco Milanese
Marco Milanese
Francesco Parolini
Francesco Parolini
Jérôme Boillot
Jérôme Boillot
Abdelraouf Ouadjaout
Abdelraouf Ouadjaout
Antoine Miné
Antoine Miné
PDF DOI

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.