Travelled to:1 × Canada
1 × Cyprus
1 × Ireland
1 × Japan
1 × The Netherlands
2 × Austria
2 × Finland
3 × Italy
3 × Spain
7 × United Kingdom
9 × USA
Collaborated with:M.B.Dwyer Robby V.P.Ranganath G.Jung X.Deng J.Belt O.Danvy E.Rodríguez T.Amtoft P.Chalin S.Laubach J.C.Corbett M.Mizuno ∅ H.Zheng M.Hoosier G.Jayaraman R.Glück J.Jørgensen G.Barthe M.H.Sørensen C.S.Pasareanu B.R.Larson K.Fowler J.Delange H.Thiagarajan A.Banerjee S.Sokolowski D.Hardin J.Hoag D.Greve T.Wallentine C.Flanagan G.T.Leavens W.Deng R.Joehanes W.Visser P.Courtieu M.Aponte T.Crolard Z.Zhang J.Guitton T.Jennings A.Childs J.Greenwald P.Shanti G.Singh
Talks about:program (13) model (13) check (11) framework (9) use (9) verif (8) softwar (6) specif (6) orient (6) compon (6)
Person: John Hatcliff
DBLP: Hatcliff:John
Facilitated 2 volumes:
Ed
EdContributed to:
2013
20132012
2012
2011
2010
2008
20072010
2007
20062006
2005
20052005
2005
200420042004
2004
2003200320032002200120001999
1999
1998
199819971995
19941992Wrote 38 papers:
- HILT-2013-CourtieuACZRBHG #coq #formal method #runtime #semantics #towards #using
- Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq (PC, MVA, TC, ZZ, R, JB, JH, JG, TJ), pp. 21–22.
- HILT-2013-LarsonHFD #fault #modelling #safety #using
- Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device (BRL, JH, KF, JD), pp. 65–84.
- ICSE-2013-HatcliffRCB #execution #framework #symbolic computation #verification
- Explicating symbolic execution (xSymExe): an evidence-based verification framework (JH, R, PC, JB), pp. 222–231.
- HILT-2012-BeltCHR #ada #automation #contract #using #verification
- Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan (JB, PC, JH, R), pp. 3–4.
- SCAM-2012-ThiagarajanHBR #contract #data flow #developer
- Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK (HT, JH, JB, R), pp. 132–137.
- SIGAda-2011-BeltHRCHD #contract #execution #symbolic computation #using
- Enhancing spark’s contract checking facilities using symbolic execution (JB, JH, R, PC, DH, XD), pp. 47–60.
- ESOP-2010-AmtoftHR #array #automation #certification #contract #data flow #precise #reasoning #source code #verification
- Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays (TA, JH, ER), pp. 43–63.
- FM-2008-AmtoftHRRHG #contract #data flow #specification
- Specification and Checking of Software Contracts for Conditional Information Flow (TA, JH, ER, R, JH, DG), pp. 229–245.
- GPCE-2007-JungH #architecture #component #framework #scalability #specification
- A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures (GJ, JH), pp. 33–42.
- GPCE-J-2007-JungH10 #architecture #component #framework #scalability #specification
- A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures (GJ, JH), pp. 615–637.
- SEFM-2007-DengRH #algorithm #execution #object-oriented #source code #symbolic computation #towards
- Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs (XD, R, JH), pp. 273–282.
- ASE-2006-RobbyDH #framework #model checking #using
- Domain-specific Model Checking Using The Bogor Framework (R, MBD, JH), pp. 369–370.
- TACAS-2006-DwyerHHRRW #concurrent #effectiveness #object-oriented #reduction #slicing #source code
- Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs (MBD, JH, MH, VPR, R, TW), pp. 73–89.
- CAV-2005-DwyerHHR #framework #model checking #using
- Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework (MBD, JH, MH, R), pp. 148–152.
- ECOOP-2005-RodriguezDFHLR #composition #concurrent #ml #multi #source code #specification #thread #verification
- Extending JML for Modular Specification and Verification of Multi-threaded Programs (ER, MBD, CF, JH, GTL, R), pp. 551–576.
- ESOP-2005-RanganathABDH #slicing
- A New Foundation for Control-Dependence and Slicing for Modern Program Structures (VPR, TA, AB, MBD, JH), pp. 77–93.
- FASE-2005-JayaramanRH #eclipse #java #named #slicing
- Kaveri: Delivering the Indus Java Program Slicer to Eclipse (GJ, VPR, JH), pp. 269–272.
- CC-2004-RanganathH #concurrent #dependence #java #slicing #source code
- Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs (VPR, JH), pp. 39–56.
- FASE-2004-ChildsGRDDHJSS #analysis #component #development #ide #named #synthesis #verification
- Cadena: An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-Based Systems (AC, JG, VPR, XD, MBD, JH, GJ, PS, GS), pp. 160–164.
- FASE-2004-JungHR #component #corba #correlation #framework
- A Correlation Framework for the CORBA Component Model (GJ, JH, VPR), pp. 144–159.
- TACAS-2004-DengDHM #aspect-oriented #framework #named
- SyncGen: An Aspect-Oriented Framework for Synchronization (XD, MBD, JH, MM), pp. 158–162.
- TACAS-2004-RobbyRDH #framework #model checking #specification #using
- Checking Strong Specifications Using an Extensible Software Model Checking Framework (R, ER, MBD, JH), pp. 404–420.
- VMCAI-2004-HatcliffRD #concurrent #model checking #object-oriented #specification #using #verification
- Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking (JH, R, MBD), pp. 175–190.
- ESEC-FSE-2003-RobbyDH #framework #model checking #named
- Bogor: an extensible and highly-modular software model checking framework (R, MBD, JH), pp. 267–276.
- ICSE-2003-HatcliffDDJR #analysis #component #development #named #verification
- Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems (JH, XD, MBD, GJ, VPR), pp. 160–173.
- PEPM-2003-HatcliffDDJRR #component #corba #design #partial evaluation #slicing
- Slicing and partial evaluation of CORBA component model designs for avionics system (JH, WD, MBD, GJ, VPR, R), pp. 1–2.
- ICSE-2002-DengDHM #concurrent #invariant #source code #specification #synthesis #verification
- Invariant-based specification, synthesis, and verification of synchronization in concurrent programs (XD, MBD, JH, MM), pp. 442–452.
- ICSE-2001-DwyerHJLPRZV #abstraction #finite #verification
- Tool-Supported Program Abstraction for Finite-State Verification (MBD, JH, RJ, SL, CSP, R, HZ, WV), pp. 177–187.
- ICSE-2000-CorbettDHLPRZ #finite #java #modelling #named #source code
- Bandera: extracting finite-state models from Java source code (JCC, MBD, JH, SL, CSP, R, HZ), pp. 439–448.
- ICSE-2000-CorbettDHR #interface #java #model checking #named #source code
- Bandera: a source-level interface for model checking Java programs (JCC, MBD, JH, R), pp. 762–765.
- PEPM-1999-DwyerH #slicing
- Slicing Software for Model Construction (MBD, JH), pp. 105–118.
- SAS-1999-HatcliffCDSZ #concurrent #formal method #multi #slicing #source code #thread #virtual machine
- A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives (JH, JCC, MBD, SS, HZ), pp. 1–18.
- ALP-PLILP-1998-HatcliffDL #analysis #staging #using
- Staging Static Analyses Using Abstraction-Based Program Specialization (JH, MBD, SL), pp. 134–151.
- LOPSTR-1998-GluckHJ #online
- Generalization in Hierarchies of Online Program Specialization Systems (RG, JH, JJ), pp. 179–198.
- PLILP-1997-BartheHS
- Reflections on Reflections (GB, JH, MHS), pp. 241–258.
- PLILP-1995-Hatcliff #correctness #verification
- Mechanically Verifying the Correctness of an Offline Partial Evaluator (JH), pp. 279–298.
- POPL-1994-HatcliffD #continuation
- A Generic Account of Continuation-Passing Styles (JH, OD), pp. 458–471.
- WSA-1992-DanvyH
- Thunks (Continued) (OD, JH), pp. 3–11.