BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × China
1 × Hungary
1 × Israel
1 × Spain
1 × Switzerland
1 × United Kingdom
2 × Denmark
2 × Finland
2 × Greece
2 × India
21 × USA
3 × Canada
3 × The Netherlands
4 × Italy
5 × France
Collaborated with:
B.Boigelot R.Jagadeesan G.Bruns P.Wolper L.J.Jagadeesan N.Klarlund D.Pirottin M.Y.Levin S.Khurshid M.Christakis M.Yannakakis A.Taly D.Luchaup J.Kinder K.Etessami N.Piterman M.Huth C.Flanagan A.P.Sistla D.E.Long K.Sen N.Tillmann E.Bounimova D.A.Molnar S.K.Lahiri C.Rubio-González B.Elkarablieh R.Xu R.Majumdar A.Kiezun S.Anand L.d.Alfaro S.Chandra C.Palm M.Benedikt T.W.Reps R.S.Hanmer C.Colby D.Peled M.G.Staskauskas G.J.Holzmann H.Peleg R.Singh A.V.Nori S.K.Rajamani S.Tetali J.D.Herbsleb D.Li K.Läufer B.Willems C.Cadar C.S.Pasareanu W.Visser
Talks about:
model (19) check (17) test (12) use (10) program (8) partial (8) dynam (7) softwar (6) automat (6) analysi (6)

Person: Patrice Godefroid

DBLP DBLP: Godefroid:Patrice

Contributed to:

VMCAI 20152015
ICSE 20142014
ICSE 20132013
TACAS 20132013
PLDI 20122012
ICSE 20112011
ISSTA 20112011
PLDI 20112011
SAS 20112011
TAP 20112011
ISSTA 20102010
POPL 20102010
ISSTA 20092009
VMCAI 20092009
ISSTA 20082008
PLDI 20082008
TACAS 20082008
POPL 20072007
IFM 20052005
LICS 20052005
PLDI 20052005
POPL 20052005
ICALP 20042004
LICS 20042004
PASTE 20042004
VMCAI 20032003
CAV 20022002
ICSE 20022002
TACAS 20022002
CAV 20012001
ICALP 20012001
LICS 20012001
CSCW 20002000
FSE 20002000
CAV 19991999
ISSTA 19981998
PLDI 19981998
CAV 19971997
POPL 19971997
SAS 19971997
TACAS 19971997
CAV 19961996
FME 19961996
ISSTA 19961996
LICS 19961996
CAV 19931993
CAV 19921992
CAV 19911991
LICS 19911991
CAV 19901990
ASE 20172017

Wrote 52 papers:

VMCAI-2015-ChristakisG #composition #image #memory management #parsing #proving #safety #testing #using
Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing (MC, PG), pp. 373–392.
ICSE-2014-Godefroid #execution
Micro execution (PG), pp. 539–549.
ICSE-2013-BounimovaGM #constraints #testing
Billions and billions of constraints: whitebox fuzz testing in production (EB, PG, DAM), pp. 122–131.
TACAS-2013-GodefroidY #analysis #source code
Analysis of Boolean Programs (PG, MY), pp. 214–229.
PLDI-2012-GodefroidT #automation #encoding #synthesis
Automated synthesis of symbolic instruction encodings from I/O samples (PG, AT), pp. 441–452.
ICSE-2011-CadarGKPSTV #assessment #execution #symbolic computation #testing
Symbolic execution for software testing in practice: preliminary assessment (CC, PG, SK, CSP, KS, NT, WV), pp. 1066–1071.
ISSTA-2011-GodefroidL #automation #generative #summary #testing
Automatic partial loop summarization in dynamic test generation (PG, DL), pp. 23–33.
PLDI-2011-Godefroid #generative #higher-order #testing
Higher-order test generation (PG), pp. 258–269.
SAS-2011-GodefroidLR #composition #generative #incremental #summary #testing #validation
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation (PG, SKL, CRG), pp. 112–128.
TAP-2011-Godefroid #proving #testing
Tests from Proofs (PG), p. 14.
ISSTA-2010-GodefroidK #float #memory management #program analysis #proving #safety
Proving memory safety of floating-point computations by combining static and dynamic program analysis (PG, JK), pp. 1–12.
POPL-2010-GodefroidNRT #composition #power of #program analysis
Compositional may-must program analysis: unleashing the power of alternation (PG, AVN, SKR, ST), pp. 43–56.
ISSTA-2009-ElkarabliehGL #generative #pointer #precise #reasoning #testing
Precise pointer reasoning for dynamic test generation (BE, PG, MYL), pp. 129–140.
VMCAI-2009-EtessamiG #programming #transaction
An Abort-Aware Model of Transactional Programming (KE, PG), pp. 59–73.
VMCAI-2009-GodefroidP #ltl #model checking #revisited
LTL Generalized Model Checking Revisited (PG, NP), pp. 89–104.
ISSTA-2008-XuGM #abstraction #testing
Testing for buffer overflows with length abstraction (RGX, PG, RM), pp. 27–38.
PLDI-2008-GodefroidKL #fuzzing #grammarware
Grammar-based whitebox fuzzing (PG, AK, MYL), pp. 206–215.
TACAS-2008-AnandGT #composition #execution #symbolic computation
Demand-Driven Compositional Symbolic Execution (SA, PG, NT), pp. 367–381.
POPL-2007-Godefroid #composition #generative #testing
Compositional dynamic test generation (PG), pp. 47–54.
IFM-2005-GodefroidK #model checking
Software Model Checking: Searching for Computations in the Abstract or the Concrete (PG, NK), pp. 20–32.
LICS-2005-GodefroidH #logic #model checking #semantics
Model Checking Vs. Generalized Model Checking: Semantic Minimizations for Temporal Logics (PG, MH), pp. 158–167.
PLDI-2005-GodefroidKS #automation #named #random testing #testing
DART: directed automated random testing (PG, NK, KS), pp. 213–223.
POPL-2005-FlanaganG #model checking #partial order #reduction
Dynamic partial-order reduction for model checking software (CF, PG), pp. 110–121.
ICALP-2004-BrunsG #logic #model checking #multi
Model Checking with Multi-valued Logics (GB, PG), pp. 281–293.
LICS-2004-AlfaroGJ #abstraction #game studies #nondeterminism #precise
Three-Valued Abstractions of Games: Uncertainty, but with Precision (LdA, PG, RJ), pp. 170–179.
PASTE-2004-Godefroid #model checking
Invited Talk: “Model checking” software with VeriSoft (PG), p. 36.
VMCAI-2003-GodefroidJ #modelling #on the
On the Expressiveness of 3-Valued Models (PG, RJ), pp. 206–222.
CAV-2002-GodefroidJ #abstraction #automation #model checking #using
Automatic Abstraction Using Generalized Model Checking (PG, RJ), pp. 137–150.
ICSE-2002-ChandraGP #case study #industrial #model checking
Software model checking in practice: an industrial case study (SC, PG, CP), pp. 431–441.
TACAS-2002-GodefroidK #algorithm #scalability #search-based #using
Exploring Very Large State Spaces Using Genetic Algorithms (PG, SK), pp. 266–280.
CAV-2001-SistlaG #model checking #symmetry
Symmetry and Reduced Symmetry in Model Checking (APS, PG), pp. 91–103.
ICALP-2001-BenediktGR #model checking #state machine #strict
Model Checking of Unrestricted Hierarchical State Machines (MB, PG, TWR), pp. 652–666.
LICS-2001-BrunsG #logic #query
Temporal Logic Query Checking (GB, PG), pp. 409–417.
CSCW-2000-GodefroidyHJL #approach #automation #privacy #verification
Ensuring privacy in presence awareness: an automated verification approach (PG, JDH, LJJ, DL), pp. 59–68.
FSE-2000-GodefroidJJL #automation #constraints #interactive #testing
Automated systematic testing for constraint-based interactive services (PG, LJJ, RJ, KL), pp. 40–49.
CAV-1999-BrunsG #logic #model checking
Model Checking Partial State Spaces with 3-Valued Temporal Logics (GB, PG), pp. 274–287.
ISSTA-1998-GodefroidHJ #analysis #model checking #monitoring #using
Model Checking Without a Model: An Analysis of the Heart-Beat Monitor of a Telephone Switch Using VeriSoft (PG, RSH, LJJ), pp. 124–133.
PLDI-1998-ColbyGJ #automation #source code
Automatically Closing Open Reactive Programs (CC, PG, LJJ), pp. 345–357.
CAV-1997-Godefroid #analysis #automation #concurrent #named
VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software (PG), pp. 476–479.
POPL-1997-Godefroid #model checking #programming language #using
Model Checking for Programming Languages using Verisoft (PG), pp. 174–186.
SAS-1997-BoigelotGWW #power of
The Power of QDDs (BB, PG, BW, PW), pp. 172–186.
TACAS-1997-BoigelotG #automation #source code #specification #synthesis
Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs (BB, PG), pp. 321–333.
CAV-1996-BoigelotG #communication #infinity #protocol #using #verification
Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (BB, PG), pp. 1–12.
FME-1996-BoigelotG #analysis #model checking #protocol #using
Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN (BB, PG), pp. 465–478.
ISSTA-1996-GodefroidPS #concurrent #industrial #partial order #source code #using #validation
Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs (PG, DP, MGS), pp. 261–269.
LICS-1996-GodefroidL #protocol #queue #verification
Symbolic Protocol Verification With Queue BDDs (PG, DEL), pp. 198–206.
CAV-1993-GodefroidP #dependence #partial order #verification
Refining Dependencies Improves Partial-Order Verification Methods (PG, DP), pp. 438–449.
CAV-1992-GodefroidHP #revisited
State-Space Caching Revisited (PG, GJH, DP), pp. 178–191.
CAV-1991-GodefroidW #concurrent #partial order #performance #safety #using #verification
Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties (PG, PW), pp. 332–342.
LICS-1991-GodefroidW #approach #model checking
A Partial Approach to Model Checking (PG, PW), pp. 406–415.
CAV-1990-Godefroid #automation #partial order #using #verification
Using Partial Orders to Improve Automatic Verification Methods (PG), pp. 176–185.
ASE-2017-GodefroidPS #fuzzing #machine learning
Learn&Fuzz: machine learning for input fuzzing (PG, HP, RS), pp. 50–59.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.