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: Godefroid:Patrice
Contributed to:
2015
20142013
2013
20122011
20112011
2011
20112010
2010200920092008200820082007
2005
200520052005
20042004
20042003
200220022002200120012001
2000
200019991998199819971997199719971996
19961996199619931992199119911990
2017Wrote 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.