Travelled to:1 × Croatia
1 × Cyprus
1 × France
1 × Ireland
1 × Spain
2 × Italy
2 × United Kingdom
3 × Germany
4 × Canada
8 × USA
Collaborated with:H.Rajan ∅ T.Wahls A.L.Baker Y.Cheon C.Chambers T.D.Millstein S.M.Shaner C.Clifton P.Müller F.Hussain C.Ruby K.K.Dhara W.E.Weihl J.M.Wing J.R.Kiniry E.Poll J.Noble D.A.Naumann T.N.Nguyen R.Dyer S.H.Tan D.Marinov L.Tan J.Tao A.Cortes M.Ceberio J.Aldrich M.Barnett D.Giannakopoulou N.Sharygina E.Rodríguez M.B.Dwyer C.Flanagan J.Hatcliff Robby J.Abrial D.S.Batory M.J.Butler A.Coglio K.Fisler E.C.R.Hehner C.B.Jones D.Miller S.L.P.Jones M.Sitaraman D.R.Smith A.Stump V.Klebanov N.Shankar V.Wüstholz E.Alkassar R.Arthan D.Bronish R.Chapman E.Cohen M.A.Hillebrand B.Jacobs K.R.M.Leino R.Monahan F.Piessens N.Polikarpova T.Ridge J.Smans S.Tobies T.Tuerk M.Ulbrich B.Weiß
Talks about:specif (11) verif (6) jml (6) modular (5) languag (5) program (4) java (4) dispatch (3) behavior (3) method (3)
Person: Gary T. Leavens
DBLP: Leavens:Gary_T=
Facilitated 4 volumes:
Ed
EdEd
EdContributed to:
2015
2012
2011
2010
2009
2008
2008
2007
20072007200720072007
20062005
20042002
20012000199919991998199619941990
1997Wrote 27 papers:
- ICSE-v2-2015-RajanNL0 #behaviour #repository #scalability #specification
- Inferring Behavioral Specifications from Large-scale Repositories by Leveraging Collective Intelligence (HR, TNN, GTL, RD), pp. 579–582.
- ICST-2012-TanMTL #consistency #detection #nondeterminism #testing
- @tComment: Testing Javadoc Comments to Detect Comment-Code Inconsistencies (SHT, DM, LT, GTL), pp. 260–269.
- FM-2011-KlebanovMSLWAABCCHJLMPPRSTTUW #case study #contest #experience
- The 1st Verified Software Competition: Experience Report (VK, PM, NS, GTL, VW, EA, RA, DB, RC, EC, MAH, BJ, KRML, RM, FP, NP, TR, JS, ST, TT, MU, BW), pp. 154–168.
- SEFM-2010-HussainL #ml #named #runtime #specification
- temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties (FH, GTL), pp. 63–72.
- ESOP-2009-RajanTSL #composition #design #named #policy #verification #web #web service
- Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services (HR, JT, SMS, GTL), pp. 333–347.
- ECOOP-2008-RajanL #named #quantifier
- Ptolemy: A Language with Quantified, Typed Events (HR, GTL), pp. 155–179.
- SEKE-2008-CheonCLC #constraints #performance #random testing #testing
- Integrating Random Testing with Constraints for Improved Efficiency and Diversity (YC, AC, GTL, MC), pp. 861–866.
- ASE-2007-Leavens #java #ml #modelling #tutorial
- Tutorial on JML, the java modeling language (GTL), p. 573.
- CAV-2007-LeavensKP #behaviour #composition #functional #java #ml #specification #tutorial #verification
- A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java (GTL, JRK, EP), p. 37.
- ECOOP-2007-CliftonLN #aspect-oriented #effectiveness #named #reasoning
- MAO: Ownership and Effects for More Effective Reasoning About Aspects (CC, GTL, JN), pp. 451–475.
- ESEC-FSE-2007-AldrichBGLS #component #specification #verification
- Specification and verification of component-based systems 2007 (JA, MB, DG, GTL, NS), pp. 609–610.
- ICSE-2007-LeavensM #information management #interface #specification
- Information Hiding and Visibility in Interface Specifications (GTL, PM), pp. 385–395.
- OOPSLA-2007-ShanerLN #composition #higher-order #source code #verification
- Modular verification of higher-order methods with mandatory calls specified by model programs (SMS, GTL, DAN), pp. 351–368.
- GPCE-2006-LeavensABBCFHJMJSSS #roadmap #verification
- Roadmap for enhanced languages and methods to aid verification (GTL, JRA, DSB, MJB, AC, KF, ECRH, CBJ, DM, SLPJ, MS, DRS, AS), pp. 221–236.
- 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.
- PASTE-2004-Leavens #exclamation #ml
- Invited Talk: JML framed! (GTL), p. 1.
- ECOOP-2002-CheonL #approach #ml #testing
- A Simple and Practical Approach to Unit Testing: The JML and JUnit Way (YC, GTL), pp. 231–255.
- SAC-2001-WahlsL #algorithm #concurrent #constraints #modelling #semantics #source code #specification
- Formal semantics of an algorithm for translating model-based specifications to concurrent constraint programs (TW, GTL), pp. 567–575.
- OOPSLA-2000-CliftonLCM #composition #java #multi #named #symmetry
- MultiJava: modular open classes and symmetric multiple dispatch for Java (CC, GTL, CC, TDM), pp. 130–145.
- OOPSLA-2000-RubyL #subclass
- Safely creating correct subclasses without seeing superclass code (CR, GTL), pp. 208–228.
- FM-v2-1999-LeavensB #specification
- Enhancing the Pre- and Postcondition Technique for More Expressive Specifications (GTL, ALB), pp. 1087–1106.
- SAC-1999-LeavensWB #data flow #diagrams #semantics #specification
- Formal Semantics for SA Style Data Flow Diagram Specification Languages (GTL, TW, ALB), pp. 526–532.
- OOPSLA-1998-LeavensM #multi #tuple
- Multiple Dispatch as Dispatch on Tuples (GTL, TDM), pp. 374–387.
- ICSE-1996-DharaL #behaviour #inheritance #specification #type system
- Forcing Behavioral Subtyping through Specification Inheritance (KKD, GTL), pp. 258–267.
- OOPSLA-1994-ChambersL #multi
- Typechecking and Modules for Multi-Methods (CC, GTL), pp. 1–15.
- OOPSLA-ECOOP-1990-LeavensW #object-oriented #reasoning #source code #type system
- Reasoning about Object-Oriented Programs that Use Subtypes (GTL, WEW), pp. 212–223.
- TAPSOFT-1997-LeavensW #interface #specification
- Protective Interface Specifications (GTL, JMW), pp. 520–534.