Travelled to:1 × India
1 × Russia
1 × Spain
2 × United Kingdom
3 × Italy
4 × Canada
9 × USA
Collaborated with:∅ D.Beyer T.A.Henzinger R.Jhala R.Majumdar T.Braibant Ziv Scully N.Zeldovich P.Wang S.Cuellar B.E.Chang G.C.Necula Peng Wang 0048 D.Wang M.Lesani C.J.Bell M.Vijayaraghavan Arvind N.Dave B.Delaware C.Pit-Claudel J.Gross X.Wang D.Lazar Z.Tatlock J.G.Malecha G.Morrisett A.Shinnar R.Wisnesky H.Chen D.Ziegler T.Chajed M.F.Kaashoek
Talks about:program (9) languag (8) verif (8) certifi (5) compil (4) applic (4) type (4) web (4) function (3) abstract (3)
Person: Adam Chlipala
DBLP: Chlipala:Adam
Contributed to:
2015
2015
2015
2015
2014
201420132013
20112010201020102009200820072006
2006
2004
2004
2004
2004201720162017Wrote 26 papers:
- CAV-2015-VijayaraghavanC #composition #deduction #design #hardware #multi #verification
- Modular Deductive Verification of Multiprocessor Hardware Designs (MV, AC, A, ND), pp. 109–127.
- ICFP-2015-Chlipala #compilation #functional #optimisation
- An optimizing compiler for a purely functional web-application language (AC), pp. 10–21.
- POPL-2015-Chlipala #named #programming #web
- Ur/Web: A Simple Model for Programming the Web (AC), pp. 153–165.
- POPL-2015-Chlipala15a #case study #composition #interface #network #parallel #thread #verification #web
- From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification (AC), pp. 609–622.
- POPL-2015-DelawarePGC #data type #deduction #named #proving #synthesis
- Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant (BD, CPC, JG, AC), pp. 689–700.
- SOSP-2015-ChenZCCKZ #file system #hoare #logic #using
- Using Crash Hoare logic for certifying the FSCQ file system (HC, DZ, TC, AC, MFK, NZ), pp. 18–37.
- OOPSLA-2014-WangCC #abstraction #compilation #verification
- Compiler verification meets cross-language linking via data abstraction (PW, SC, AC), pp. 675–690.
- OSDI-2014-WangLZCT #framework #interpreter #kernel #named
- Jitk: A Trustworthy In-Kernel Interpreter Infrastructure (XW, DL, NZ, AC, ZT), pp. 33–47.
- CAV-2013-BraibantC #hardware #synthesis #verification
- Formal Verification of Hardware Synthesis (TB, AC), pp. 213–228.
- ICFP-2013-Chlipala #generative #hoare #logic #metaprogramming #verification
- The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier (AC), pp. 391–402.
- PLDI-2011-Chlipala #logic #low level #source code #verification
- Mostly-automated verification of low-level programs in computational separation logic (AC), pp. 234–245.
- OSDI-2010-Chlipala #policy #security #static analysis
- Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications (AC), pp. 105–118.
- PLDI-2010-Chlipala #metaprogramming #named #static typing
- Ur: statically-typed metaprogramming with type-level record computation (AC), pp. 122–133.
- POPL-2010-Chlipala #compilation #functional
- A verified compiler for an impure functional language (AC), pp. 93–106.
- ICFP-2009-ChlipalaMMSW #effectiveness #higher-order #imperative #interactive #proving #source code
- Effective interactive proofs for higher-order imperative programs (AC, JGM, GM, AS, RW), pp. 79–90.
- ICFP-2008-Chlipala #higher-order #parametricity #semantics #syntax
- Parametric higher-order abstract syntax for mechanized semantics (AC), pp. 143–156.
- PLDI-2007-Chlipala #assembly #compilation #λ-calculus
- A certified type-preserving compiler from λ calculus to assembly language (AC), pp. 54–65.
- ICFP-2006-Chlipala #composition #development #proving #verification
- Modular development of certified program verifiers with a proof assistant (AC), pp. 160–171.
- VMCAI-2006-ChangCN #framework #program analysis #safety
- A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety (BYEC, AC, GCN), pp. 174–189.
- ICSE-2004-BeyerCM #generative #testing
- Generating Tests from Counterexamples (DB, AC, TAH, RJ, RM), pp. 326–335.
- PEPM-2004-BeyerCHJM #query #verification
- Invited talk: the blast query language for software verification (DB, AC, TAH, RJ, RM), pp. 201–202.
- PPDP-2004-BeyerCHJM #query #verification
- Invited talk: the blast query language for software verification (DB, AC, TAH, RJ, RM), pp. 1–2.
- SAS-2004-BeyerCHJM #query #verification
- The Blast Query Language for Software Verification. (DB, AC, TAH, RJ, RM), pp. 2–18.
- OOPSLA-2017-WangWC #analysis #complexity #functional #invariant #named
- TiML: a functional language for practical complexity analysis with invariants (PW0, DW, AC), p. 26.
- POPL-2016-LesaniBC #consistency #distributed #named
- Chapar: certified causally consistent distributed key-value stores (ML, CJB, AC), pp. 357–370.
- POPL-2017-ScullyC #automation #database #optimisation
- A program optimization for automatic database result caching (ZS, AC), pp. 271–284.