Travelled to:1 × Denmark
1 × Estonia
1 × Germany
1 × Hungary
1 × India
1 × Poland
1 × Portugal
1 × Russia
1 × Turkey
11 × USA
2 × Austria
2 × Spain
3 × France
4 × Italy
4 × United Kingdom
Collaborated with:M.Chechik S.Chaki A.Albarghouthi Y.Vizel O.Wei A.Komuravelli A.Belov B.Devereux J.A.Navas M.Gheorghiu Y.Li T.Kahsai O.Strichman S.Shoham N.Bjørner E.M.Clarke T.E.Hart K.Ku D.Lie S.Malik J.Marques-Silva C.Cohen S.Nejati Y.Meshman G.Fedyukovich N.Sharygina I.Dillig S.Kong S.Ben-David S.Uchitel I.Ozkaya J.A.D.Pace R.Shemer H.G.V.Krishnan V.Ganesh Z.Kincaid S.Sapra M.Minea S.M.Easterbrook A.Y.C.Lai V.Petrovykh A.Tafliovich C.D.Thompson-Walsh Elazar Gershuni N.Amit N.Narodytska N.Rinetzky L.Ryzhyk M.Sagiv
Talks about:abstract (11) model (10) verif (8) interpol (6) check (6) program (5) base (5) framework (4) properti (4) softwar (4)
♂ Person: Arie Gurfinkel
DBLP: Gurfinkel:Arie
Facilitated 6 volumes:
DemoTrackChPrCoToChPrCoPrCoPrCoContributed to:
2015
2015
20152014
201420142013
2013201320132012
201220122012
2011
20112010
2010201020092008
2007
20072006200620062005
200520042003
2003
200320032002
200220162016201920192016
2019Wrote 46 papers:
- CAV-2015-GurfinkelKKN #framework #verification
- The SeaHorn Verification Framework (AG, TK, AK, JAN), pp. 343–361.
- CAV-2015-VizelGM #performance
- Fast Interpolating BMC (YV, AG, SM), pp. 641–657.
- TACAS-2015-GurfinkelKN #c #contest #framework #named #source code #verification
- SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (AG, TK, JAN), pp. 447–450.
- VMCAI-2015-BjornerG #abstraction
- Property Directed Polyhedral Abstraction (NB, AG), pp. 263–281.
- CAV-2014-KomuravelliGC #model checking #recursion #smt #source code
- SMT-Based Model Checking for Recursive Programs (AK, AG, SC), pp. 17–34.
- CAV-2014-VizelG #reachability
- Interpolating Property Directed Reachability (YV, AG), pp. 260–276.
- POPL-2014-LiAKGC #optimisation #smt
- Symbolic optimization with SMT solvers (YL, AA, ZK, AG, MC), pp. 607–618.
- TACAS-2014-GurfinkelB #contest #named #verification
- FrankenBit: Bit-Precise Verification with Many Bits — (Competition Contribution) (AG, AB), pp. 408–411.
- TACAS-2014-GurfinkelBM #invariant
- Synthesizing Safe Bit-Precise Invariants (AG, AB, JMS), pp. 93–108.
- CAV-2013-KomuravelliGCC #abstraction #automation #bound #model checking #smt
- Automatic Abstraction in SMT-Based Unbounded Software Model Checking (AK, AG, SC, EMC), pp. 846–862.
- ICTSS-2013-SapraMCGC #execution #fault #python #source code #symbolic computation #using
- Finding Errors in Python Programs Using Dynamic Symbolic Execution (SS, MM, SC, AG, EMC), pp. 283–289.
- TACAS-2013-AlbarghouthiGLCC #abstract interpretation #contest #named #verification
- UFO: Verification with Interpolants and Abstract Interpretation — (Competition Contribution) (AA, AG, YL, SC, MC), pp. 637–640.
- VMCAI-2013-ChakiGKS #composition #source code
- Compositional Sequentialization of Periodic Programs (SC, AG, SK, OS), pp. 536–554.
- CAV-2012-AlbarghouthiLGC #framework #named #verification
- Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification (AA, YL, AG, MC), pp. 672–678.
- SAS-2012-AlbarghouthiGC
- Craig Interpretation (AA, AG, MC), pp. 300–316.
- TACAS-2012-AlbarghouthiGC #approximate
- From Under-Approximations to Over-Approximations and Back (AA, AG, MC), pp. 157–172.
- VMCAI-2012-AlbarghouthiGC #algorithm #interprocedural #named #verification
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification (AA, AG, MC), pp. 39–55.
- VMCAI-2012-ChakiGS #concurrent #multi #source code #thread #verification
- Regression Verification for Multi-threaded Programs (SC, AG, OS), pp. 119–135.
- ESEC-FSE-2011-Ben-DavidCGU #logic #named #specification
- CSSL: a logic for specifying conditional scenarios (SBD, MC, AG, SU), pp. 37–47.
- KDD-2011-ChakiCG #learning
- Supervised learning for provenance-similarity of binaries (SC, CC, AG), pp. 15–23.
- CAV-2010-AlbarghouthiGWC #analysis #symbolic computation
- Abstract Analysis of Symbolic Executions (AA, AG, OW, MC), pp. 495–510.
- CSMR-2010-OzkayaPGC #architecture #evolution #requirements #using
- Using Architecturally Significant Requirements for Guiding System Evolution (IO, JADP, AG, SC), pp. 127–136.
- SAS-2010-GurfinkelC #abstract domain #named
- Boxes: A Symbolic Abstract Domain of Boxes (AG, SC), pp. 287–303.
- VMCAI-2009-WeiGC #revisited
- Mixed Transition Systems Revisited (OW, AG, MC), pp. 349–365.
- ASE-2008-HartKGCL #abstraction #proving #refinement
- Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates (TEH, KK, AG, MC, DL), pp. 387–390.
- ASE-2008-HartKGCL08a #model checking #named #proving
- PtYasm: Software Model Checking with Proof Templates (TEH, KK, AG, MC, DL), pp. 479–480.
- FASE-2007-ChechikGG
- Finding Environment Guarantees (MC, MG, AG), pp. 352–367.
- IFM-2007-GheorghiuGC #logic #query
- Finding State Solutions to Temporal Logic Queries (MG, AG, MC), pp. 273–292.
- CAV-2006-GurfinkelWC #model checking #named #verification
- Yasm: A Software Model-Checker for Verification and Refutation (AG, OW, MC), pp. 170–174.
- TACAS-2006-GurfinkelC #abstraction #question #why
- Why Waste a Perfectly Good Abstraction? (AG, MC), pp. 212–226.
- VMCAI-2006-GurfinkelWC #abstraction #model checking
- Systematic Construction of Abstractions for Model-Checking (AG, OW, MC), pp. 381–397.
- FASE-2005-ChechikG #framework #generative
- A Framework for Counterexample Generation and Exploration (MC, AG), pp. 220–236.
- SEFM-2005-NejatiGC #abstraction
- Stuttering Abstraction for Model Checkin (SN, AG, MC), pp. 311–320.
- TACAS-2004-GurfinkelC #how #question
- How Vacuous Is Vacuous? (AG, MC), pp. 451–466.
- CAV-2003-ChechikG #logic #named #query
- TLQSolver: A Temporal Logic Query Checker (MC, AG), pp. 210–214.
- FME-2003-GurfinkelC #generative #model checking #multi
- Generating Counterexamples for Multi-valued Model-Checking (AG, MC), pp. 503–521.
- ICSE-2003-EasterbrookCDGLPTT #model checking #multi #named #reasoning
- χChek: A Model Checker for Multi-Valued Reasoning (SME, MC, BD, AG, AYCL, VP, AT, CDTW), pp. 804–805.
- TACAS-2003-GurfinkelC #proving
- Proof-Like Counter-Examples (AG, MC), pp. 160–175.
- CAV-2002-ChechikGD #model checking #multi #named
- chi-Chek: A Multi-valued Model-Checker (MC, AG, BD), pp. 505–509.
- FSE-2002-GurfinkelDC #logic #query
- Model exploration with temporal logic query checking (AG, BD, MC), pp. 139–148.
- FSE-2016-GurfinkelSM #smt #verification
- SMT-based verification of parameterized systems (AG, SS, YM), pp. 338–348.
- CAV-2016-FedyukovichGS #equivalence #simulation
- Property Directed Equivalence via Abstract Simulation (GF, AG, NS), pp. 433–453.
- CAV-2019-ShemerGSV #composition
- Property Directed Self Composition (RS, AG, SS, YV), pp. 161–179.
- CAV-2019-KrishnanVGG #induction
- Interpolating Strong Induction (HGVK, YV, VG, AG), pp. 367–385.
- POPL-2016-AlbarghouthiDG #specification #synthesis
- Maximal specification synthesis (AA, ID, AG), pp. 789–801.
- PLDI-2019-GershuniAGNNRRS #kernel #linux #precise #static analysis
- Simple and precise static analysis of untrusted Linux kernel extensions (EG, NA, AG, NN, JAN, NR, LR, MS), pp. 1069–1084.