static analysis

Mathematical Programming: Turing completeness and applications to software analysis

  • Leo Liberti
  • Fabrizio Marinelli
    • Categories (Mixed) Integer Nonlinear Programming, Applications - Science and Engineering, Global Optimization Applications Tags , , ,

    Mathematical Programming is Turing complete, and can be used as a general-purpose declarative language. We present a new constructive proof of this fact, and showcase its usefulness by discussing an application to finding the hardest input of any given program running on a Minsky Register Machine. We also discuss an application of Mathematical Programming to … Read more

    Code verification by static analysis: a mathematical programming approach

  • Stephane Le Roux
  • Leo Liberti
  • Fabrizio Marinelli
  • Jeremy Leconte
    • Categories (Mixed) Integer Nonlinear Programming, Applications - Science and Engineering, Modeling Languages and Systems Tags , , , , ,

    Automatic verification of computer code is of paramount importance in embedded systems supplying essential services. One of the most important verification techniques is static code analysis by abstract interpretation: the concrete semantics of a programming language (i.e.the values $\chi$ that variable symbols {\tt x} appearing in a program can take during its execution) are replaced … Read more