Person: David Monniaux

DBLP: Monniaux:David

Contributed to:

2015

2015

2015

2014

2014

2013

2012

2012

2011

2011

2010

2009

2009

2007

2005

2005

2003

2003

2003

2001

2001

2001

2000

1999

2017

2019

Wrote 26 papers:

PLDI-2015-GonnordMR #ranking #synthesis #using

Synthesis of ranking functions using extremal counterexamples (LG, DM, GR), pp. 608–618.

SAC-2015-AlbertiM #array

Polyhedra to the rescue of array interpolants (FA, DM), pp. 1745–1750.

SAS-2015-MonniauxA #abstraction #array

A Simple Abstraction of Arrays and Maps by Program Translation (DM, FA), pp. 217–234.

LCTES-2014-HenryAMM #encoding #execution #how #modulo theories #optimisation #semantics #worst-case

How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics (JH, MA, DM, CM), pp. 43–52.

SAS-2014-MonniauxS

Speeding Up Logico-Numerical Strategy Iteration (DM, PS), pp. 253–267.

SAS-2013-FouilheMP #abstract domain #correctness #generative #performance

Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra (AF, DM, MP), pp. 345–365.

SAS-2012-HenryMM #abstract interpretation #algorithm #analysis #evaluation

Succinct Representations for Abstract Interpretation — Combined Analysis Algorithms and Experimental Evaluation (JH, DM, MM), pp. 283–299.

SMT-2012-PhanBM #quantifier #satisfiability

Anatomy of Alternating Quantifier Satisfiability (ADP, NB, DM), pp. 120–130.

ESOP-2011-GawlitzaM #smt

Improving Strategies via SMT Solving (TMG, DM), pp. 236–255.

SAS-2011-MonniauxG #bound #fixpoint #model checking #using

Using Bounded Model Checking to Focus Fixpoint Iterations (DM, LG), pp. 369–385.

CAV-2010-Monniaux #lazy evaluation #quantifier

Quantifier Elimination by Lazy Model Enumeration (DM), pp. 585–599.

CAV-2009-Monniaux #float #linear #on the #using

On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure (DM), pp. 570–583.

POPL-2009-Monniaux #abstraction #automation #composition #constraints #linear

Automatic modular abstractions for linear constraints (DM), pp. 140–151.

SAS-2007-Monniaux #abstraction #source code

Optimal Abstraction on Real-Valued Programs (DM), pp. 104–120.

CAV-2005-Monniaux #analysis #composition #float #linear

Compositional Analysis of Floating-Point Linear Numerical Filters (DM), pp. 199–212.

ESOP-2005-CousotCFMMMR

The ASTREÉ Analyzer (PC, RC, JF, LM, AM, DM, XR), pp. 21–30.

PLDI-2003-BlanchetCCFMMMR #safety #scalability

A static analyzer for large safety-critical software (BB, PC, RC, JF, LM, AM, DM, XR), pp. 196–207.

SAS-2003-Monniaux #abstract interpretation #markov #process #source code

Abstract Interpretation of Programs as Markov Decision Processes (DM), pp. 237–254.

VMCAI-2003-Monniaux #abstraction #using

Abstraction of Expectation Functions Using Gaussian Distributions (DM), pp. 161–173.

ESOP-2001-Monniaux #abstract interpretation #probability #source code

Backwards Abstract Interpretation of Probabilistic Programs (DM), pp. 367–382.

POPL-2001-Monniaux #analysis #monte carlo #probability #source code

An abstract Monte-Carlo method for the analysis of probabilistic programs (DM), pp. 93–101.

SAS-2001-Monniaux #analysis #probability #source code #termination

An Abstract Analysis of the Probabilistic Termination of Programs (DM), pp. 111–126.

SAS-2000-Monniaux #abstract interpretation #probability #semantics

Abstract Interpretation of Probabilistic Semantics (DM), pp. 322–339.

SAS-1999-Monniaux #automaton #encryption #protocol

Abstracting Cryptographic Protocols with Tree Automata (DM), pp. 149–163.

CAV-2017-TouzeauMMR #analysis #nondeterminism #performance

Ascertaining Uncertainty for Efficient Exact Cache Analysis (VT, CM, DM, JR), pp. 22–40.

POPL-2019-TouzeauMMR #analysis #performance

Fast and exact analysis for LRU caches (VT, CM, DM, JR), p. 29.