Search results for "JML"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
148	Gary T. Leavens	Invited Talk: JML framed!	PASTE	2004	DBLP DOI BibTeX RDF
144	Patrice Chalin	Improving JML: For a Safer and More Effective Language.	FME	2003	DBLP DOI BibTeX RDF	behavioral interface specification languages, specification language design and semantics, arbitrary precision numeric types, assertion-based languages, formal methods, JML, Java Modeling Language
129	Gary T. Leavens	Tutorial on JML, the java modeling language.	ASE	2007	DBLP DOI BibTeX RDF	java modeling language (JML), model field, specification inheritance, verification, specification, tool, invariant, information hiding, assertion, design by contract, extended static checking, behavioral subtype, runtime assertion checking
116	Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert	Checking JML Specifications with B Machines.	ZB	2005	DBLP DOI BibTeX RDF	object-oriented, specifications, B method, abstract machines, JML, Java Modeling Language
114	Henrique Rebêlo, Sérgio Soares, Ricardo Massa Ferreira Lima, Leopoldo Ferreira, Márcio Cornélio	Implementing Java modeling language contracts with AspectJ.	SAC	2008	DBLP DOI BibTeX RDF	JML compiler, aspect-oriented programming, AspectJ, design by contract, JML language
109	Henrique Rebêlo, Ricardo Massa Ferreira Lima, Márcio Cornélio, Sérgio Soares	A JML Compiler Based on AspectJ.	ICST	2008	DBLP DOI BibTeX RDF	JML compiler, Aspect-Oriented Programming, AspectJ, Design by Contract, JML language
107	Bart Jacobs 0001, Erik Poll	A Logic for the Java Modeling Language JML.	FASE	2001	DBLP DOI BibTeX RDF
102	Leo Freitas, Jim Woodcock 0001	Proving Theorems About JML Classes.	Formal Methods and Hybrid Real-Time Systems	2007	DBLP DOI BibTeX RDF	Grand Challenge in Verified Software, Java Collections Framework, Java HashMap class, linking theories, Z/Eves, formal specification, Z, software verification, JML, Java Modeling Language, mechanical theorem proving, Verified Software Repository
93	Patrice Chalin, Perry R. James, George Karabotsos	An integrated verification environment for JML: architecture and early results.	SAVCBS	2007	DBLP DOI BibTeX RDF	JML4, integrated verification environment, Eclipse, java modeling language
93	Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll	An overview of JML tools and applications.	Int. J. Softw. Tools Technol. Transf.	2005	DBLP DOI BibTeX RDF	Assertion checking, Java, Formal specification, Program verification, Design by Contract
93	Guoqing Xu, Zongyuang Yang	JMLAutoTest: A Novel Automated Testing Framework Based on JML and JUnit.	FATES	2003	DBLP DOI BibTeX RDF
93	Kerry Trentelman, Marieke Huisman	Extending JML Specifications with Temporal Logic.	AMAST	2002	DBLP DOI BibTeX RDF
92	Yoonsik Cheon, Gary T. Leavens	A contextual interpretation of undefinedness for runtime assertion checking.	AADEBUG	2005	DBLP DOI BibTeX RDF	undefinedness, formal methods, exceptions, JML language, runtime assertion checking, partial functions
79	Patrice Chalin, Frédéric Rioux	JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity.	FM	2008	DBLP DOI BibTeX RDF
79	Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert	JML2B: Checking JML Specifications with B Machines.	B	2007	DBLP DOI BibTeX RDF
79	Gary T. Leavens, Albert L. Baker, Clyde Ruby	Preliminary design of JML: a behavioral interface specification language for java.	ACM SIGSOFT Softw. Eng. Notes	2006	DBLP DOI BibTeX RDF
79	Ali Hamie	On the Relationship between the Object Constraint Language (OCL) and the Java Modeling Language (JML).	PDCAT	2006	DBLP DOI BibTeX RDF
79	Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby	Extending JML for Modular Specification and Verification of Multi-threaded Programs.	ECOOP	2005	DBLP DOI BibTeX RDF
79	David R. Cok, Joseph Kiniry	ESC/Java2: Uniting ESC/Java and JML.	CASSIS	2004	DBLP DOI BibTeX RDF
70	Jianjun Zhao 0001, Martin C. Rinard	Pipa: A Behavioral Interface Specification Language for AspectJ.	FASE	2003	DBLP DOI BibTeX RDF
65	Patrice Chalin, Frédéric Rioux	Non-null references by default in the Java modeling language.	ACM SIGSOFT Softw. Eng. Notes	2006	DBLP DOI BibTeX RDF	non-null references, reference types, contracts, JML, java modeling language
65	Ali Hamie	Translating the Object Constraint Language into the Java Modelling Language.	SAC	2004	DBLP DOI BibTeX RDF	UML, constraints, reasoning, OCL, JML
65	Patrice Chalin, Perry R. James, George Karabotsos	JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML.	VSTTE	2008	DBLP DOI BibTeX RDF
65	Gary T. Leavens	JML's Rich, Inherited Specifications for Behavioral Subtypes.	ICFEM	2006	DBLP DOI BibTeX RDF
65	Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard	Automated Boundary Test Generation from JML Specifications.	FM	2006	DBLP DOI BibTeX RDF	boundary values, Test generation, automated, model-based, Java Modeling Language
65	Guillaume Dufay, Amy P. Felty, Stan Matwin	Privacy-Sensitive Information Flow with JML.	CADE	2005	DBLP DOI BibTeX RDF
65	Lydie du Bousquet, Yves Ledru, Olivier Maury, Catherine Oriat, Jean-Louis Lanet	Case Study in JML-Based Software Validation.	ASE	2004	DBLP DOI BibTeX RDF
65	Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok	How the Design of JML Accomodates Both Runtime Assertion Checking and Formal Verification.	FMCO	2002	DBLP DOI BibTeX RDF
60	Néstor Cataño, Tim Wahls	Executing JML specifications of Java card applications: a case study.	SAC	2009	DBLP DOI BibTeX RDF	executable specifications, Java card, JML
60	John Lloyd, Jan Jürjens	Security Analysis of a Biometric Authentication System Using UMLsec and JML.	MoDELS	2009	DBLP DOI BibTeX RDF	UMLsec, Security analysis, biometric authentication, JML
60	Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Mark Utting	JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP.	TACAS	2005	DBLP DOI BibTeX RDF	symbolic animation, object-oriented, model-based, Java Modeling Language
56	Catherine Oriat	Jartege: A Tool for Random Generation of Unit Tests for Java Classes.	QoSA/SOQUA	2005	DBLP DOI BibTeX RDF
51	Claude Marché, Nicolas Rousset	Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears.	SEFM	2006	DBLP DOI BibTeX RDF	JAVA CARD applets, Card Tears, non-atomic methods, Formal verification, Transactions, JML
51	Yves Ledru, Lydie du Bousquet, Olivier Maury, Pierre Bontron	Filtering TOBIAS Combinatorial Test Suites.	FASE	2004	DBLP DOI BibTeX RDF	VDM, combinatorial testing, JML, model-based specifications
51	Gary T. Leavens, Joseph R. Kiniry, Erik Poll	A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java.	CAV	2007	DBLP DOI BibTeX RDF
51	Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff	Checking JML specifications using an extensible software model checking framework.	Int. J. Softw. Tools Technol. Transf.	2006	DBLP DOI BibTeX RDF
51	Maciej Cielecki, Jedrzej Fulara, Krzysztof Jakubczyk, Lukasz Jancewicz	Propagation of JML non-null annotations in Java programs.	PPPJ	2006	DBLP DOI BibTeX RDF
51	Alain Giorgetti, Julien Groslambert	JAG: JML Annotation Generation for Verifying Temporal Properties	FASE	2006	DBLP DOI BibTeX RDF
51	Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Mark Utting	Symbolic Animation of JML Specifications.	FM	2005	DBLP DOI BibTeX RDF
51	Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll	Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2.	FMCO	2005	DBLP DOI BibTeX RDF
51	Roy Patrick Tan, Stephen H. Edwards	Experiences evaluating the effectiveness of JML-JUnit testing.	ACM SIGSOFT Softw. Eng. Notes	2004	DBLP DOI BibTeX RDF
46	Frédéric Dadeau	Evaluation Symbolique à Contraintes pour la Validation - Application à Java/JML. (Constrained Symbolic Evaluation for Validation - Application to Java/JML).		2006	RDF
42	Martin T. Vechev, Eran Yahav, Greta Yorsh	PHALANX: parallel checking of expressive heap assertions.	ISMM	2010	DBLP DOI BibTeX RDF	parallel garbage collector, virtual machine, ownership
42	Ilkay Sari, Erchin Serpedin, Kyoung-Lae Noh, Qasim M. Chaudhari, Bruce W. Suter	On the Joint Synchronization of Clock Offset and Skew in RBS-Protocol.	IEEE Trans. Commun.	2008	DBLP DOI BibTeX RDF
42	Seongwook Song, Andrew C. Singer	Blind OFDM Channel Estimation Using FIR Constraints: Reduced Complexity and Identifiability.	IEEE Trans. Inf. Theory	2007	DBLP DOI BibTeX RDF
42	Lilian Burdy, Marieke Huisman, Mariela Pavlova	Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode.	FASE	2007	DBLP DOI BibTeX RDF
42	Lilian Burdy, Mariela Pavlova	Java bytecode specification and verification.	SAC	2006	DBLP DOI BibTeX RDF
42	Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert, Jacques Julliand	Safety Property Driven Test Generation from.	FATES/RV	2006	DBLP DOI BibTeX RDF	JavaCard, automated testing, black-box testing, safety properties, Java Modeling Language
42	Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff, Robby	A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking.	CASSIS	2004	DBLP DOI BibTeX RDF
37	David Briggs, Suad Alagic	Algebraic specification techniques for parametric types with logic-based constraints.	SAC	2009	DBLP DOI BibTeX RDF	parametric types, verification theories, assertions, PVS, JML
37	Erik Poll	Teaching Program Specification and Verification Using JML and ESC/Java2.	TFM	2009	DBLP DOI BibTeX RDF
37	Marieke Huisman, Alejandro Tamalet	A Formal Connection between Security Automata and JML Annotations.	FASE	2009	DBLP DOI BibTeX RDF
37	Wladimir Araujo, Lionel C. Briand, Yvan Labiche	Concurrent Contracts for Java in JML.	ISSRE	2008	DBLP DOI BibTeX RDF
37	Lennart Beringer, Martin Hofmann 0001	A Bytecode Logic for JML and Types.	APLAS	2006	DBLP DOI BibTeX RDF
37	Ben Krause, Tim Wahls	jmle: A Tool for Executing JML Specifications Via Constraint Programming.	FMICS/PDMC	2006	DBLP DOI BibTeX RDF
37	Gary T. Leavens, Curtis Clifton	Lessons from the JML Project.	VSTTE	2005	DBLP DOI BibTeX RDF
37	Yoonsik Cheon, Gary T. Leavens	A Simple and Practical Approach to Unit Testing: The JML and JUnit Way.	ECOOP	2002	DBLP DOI BibTeX RDF
37	Joachim van den Berg, Bart Jacobs 0001	The LOOP Compiler for Java and JML.	TACAS	2001	DBLP DOI BibTeX RDF
36	Ghaith Haddad, Faraz Hussain 0001, Gary T. Leavens	The design of SafeJML, a specification language for SCJ with support for WCET specification.	JTRES	2010	DBLP DOI BibTeX RDF	SafeJML, java modeling language (JML), safety critical Java (SCJ), performance, WCET, timing behavior, duration
36	Yoonsik Cheon, Ashaveena Perumandla	Specifying and checking method call sequences of Java programs.	Softw. Qual. J.	2007	DBLP DOI BibTeX RDF	Method call sequence specification, Programming by contract, Assertion, Pre and postconditions, Runtime checking, JML language
36	Clyde Ruby, Gary T. Leavens	Safely creating correct subclasses without seeing superclass code.	OOPSLA	2000	DBLP DOI BibTeX RDF	downcalls, method refinement, semantic fragile subclassing problem, specification inheritance, subclassing contract, Java, Java language, subclass, JML language
28	Piotr Kosiuczenko	On the Implementation of @pre.	FASE	2009	DBLP DOI BibTeX RDF
28	Jacek Chrzaszcz, Marieke Huisman, Aleksy Schubert	BML and Related Tools.	FMCO	2008	DBLP DOI BibTeX RDF
28	Wen Jiang 0005, Geoffrey Ye Li, Xingxing Yu	Truncation for Low-Complexity MIMO Signal Detection.	IEEE Trans. Inf. Theory	2007	DBLP DOI BibTeX RDF
28	Gregor Engels, Baris Güldali, Marc Lohmann	Towards Model-Driven Unit Testing.	MoDELS (Workshops)	2006	DBLP DOI BibTeX RDF	visual contracts, model checking, test case generation, Design by Contract
28	Orhan Coskun, Keith M. Chugg	Combined Coding and Training for Unknown ISI Channels.	IEEE Trans. Commun.	2005	DBLP DOI BibTeX RDF
28	Marc Lohmann, Stefan Sauer 0001, Gregor Engels	Executable Visual Contracts.	VL/HCC	2005	DBLP DOI BibTeX RDF
28	Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff	Checking Strong Specifications Using an Extensible Software Model Checking Framework.	TACAS	2004	DBLP DOI BibTeX RDF
28	Engelbert Hubbers	Integrating Tools for Automatic Program Verification.	Ershov Memorial Conference	2003	DBLP DOI BibTeX RDF
23	Mikolás Janota, Radu Grigore, Michal Moskal	Reachability analysis for annotated code.	SAVCBS	2007	DBLP DOI BibTeX RDF	ESC/Java2, JML
23	Gary T. Leavens, David R. Cok, Amirfarhad Nilizadeh	Further Lessons from the JML Project.	The Logic of Software. A Tasting Menu of Formal Methods	2022	DBLP DOI BibTeX RDF
23	Armand Puccetti, Gaël de Chalendar, Pierre-Yves Gibello	Combining formal and machine learning techniques for the generation of JML specifications.	FTfJP@ECOOP	2021	DBLP DOI BibTeX RDF
23	Steven Monteiro, Erikas Sokolovas, Ellen Wittingen, Tom van Dijk, Marieke Huisman	IntelliJML: a JML plugin for IntelliJ IDEA.	FTfJP@ECOOP	2021	DBLP DOI BibTeX RDF
23	David R. Cok	JML and OpenJML for Java 16.	FTfJP@ECOOP	2021	DBLP DOI BibTeX RDF
23	Bernhard Beckert, Michael Kirsten, Jonas Klamroth, Mattias Ulbrich	Modular Verification of JML Contracts Using Bounded Model Checking.	ISoLA (1)	2020	DBLP DOI BibTeX RDF
23	Peter W. V. Tran-Jørgensen, Peter Gorm Larsen, Gary T. Leavens	Automated translation of VDM to JML-annotated Java.	Int. J. Softw. Tools Technol. Transf.	2018	DBLP DOI BibTeX RDF
23	Ijaz Ahmed, Néstor Cataño	Checking JML-encoded finite state machine properties.	ICACS	2018	DBLP DOI BibTeX RDF
23	Yuyan Bao, Gary T. Leavens	A Methodology for Invariants, Framing, and Subtyping in JML.	Principled Software Development	2018	DBLP DOI BibTeX RDF
23	Jan Boerman, Marieke Huisman, Sebastiaan J. C. Joosten	Reasoning About JML: Differences Between KeY and OpenJML.	IFM	2018	DBLP DOI BibTeX RDF
23	Christoph Gladisch, Shmuel S. Tyszberowicz	Specifying linked data structures in JML for combining formal verification and testing.	Sci. Comput. Program.	2015	DBLP DOI BibTeX RDF
23	Gary T. Leavens	JML: Expressive Contracts, Specification Inheritance, and Behavioral Subtyping.	PPPJ	2015	DBLP DOI BibTeX RDF
23	Jorne Kandziora, Marieke Huisman, Christoph Bockisch, Marina Zaharieva-Stojanovski	Run-time assertion checking of JML annotations in multithreaded applications with e-OpenJML.	FTfJP@ECOOP	2015	DBLP DOI BibTeX RDF
23	David R. Cok	OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse.	F-IDE	2014	DBLP DOI BibTeX RDF
23	Ali Hamie	Pattern-based Mapping of OCL Specifications to JML Contracts.	MODELSWARD	2014	DBLP DOI BibTeX RDF
23	Ali Hamie	Using Patterns to Map OCL Constraints to JML Specifications.	MODELSWARD (Revised Selected Papers)	2014	DBLP DOI BibTeX RDF
23	Víctor Rivera, Néstor Cataño	Translating event-B to JML-specified Java programs.	SAC	2014	DBLP DOI BibTeX RDF
23	Daniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, Shmuel S. Tyszberowicz	Generating JML Specifications from Alloy Expressions.	Haifa Verification Conference	2014	DBLP DOI BibTeX RDF
23	Gary T. Leavens, Peter H. Schmitt, Jooyong Yi	The Java Modeling Language (JML) (NII Shonan Meeting 2013-3).	NII Shonan Meet. Rep.	2013	DBLP BibTeX RDF
23	Néstor Cataño, Camilo Rueda, Tim Wahls	A Machine-Checked Proof for a Translation of Event-B Machines to JML.	CoRR	2013	DBLP BibTeX RDF
23	Henrique Rebêlo, Ricardo Massa Ferreira Lima, Gary T. Leavens, Márcio Cornélio, Alexandre Mota 0001, César A. L. de Oliveira	Optimizing generated aspect-oriented assertion checking code for JML using program transformations: An empirical study.	Sci. Comput. Program.	2013	DBLP DOI BibTeX RDF
23	Henrique Rebêlo, Gary T. Leavens, Ricardo Massa Ferreira Lima	Client-aware checking and information hiding in interface specifications with JML/ajmlc.	SPLASH (Companion Volume)	2013	DBLP DOI BibTeX RDF
23	Hiroaki Shimba, Kentaro Hanada, Kozo Okano, Shinji Kusumoto	Bidirectional Translation between OCL and JML for Round-Trip Engineering.	APSEC (2)	2013	DBLP DOI BibTeX RDF
23	Anders P. Ravn, Hans Søndergaard	A test suite for safety-critical Java using JML.	JTRES	2013	DBLP DOI BibTeX RDF
23	Christoph Gladisch, Shmuel S. Tyszberowicz	Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking.	SBMF	2013	DBLP DOI BibTeX RDF
23	Néstor Cataño, Tim Wahls, Camilo Rueda, Víctor Rivera, Danni Yu	Translating B machines to JML specifications.	SAC	2012	DBLP DOI BibTeX RDF
23	Masahiro Sakai, Kohei Maruchi, Takeo Imai	Model-Checking C Programs against JML-like Specification Language.	APSEC	2012	DBLP DOI BibTeX RDF
23	Kentaro Hanada, Kozo Okano, Shinji Kusumoto, Kiyoyuki Miyazawa	Practical Application of a Translation Tool from UML/OCL to Java Skeleton with JML Annotation.	ICEIS (2)	2012	DBLP BibTeX RDF
23	Frédéric Dadeau, Fabien Peureux	Grey-Box Testing and Verification of Java/JML.	ICST Workshops	2011	DBLP DOI BibTeX RDF
23	David R. Cok	OpenJML: JML for Java 7 by Extending OpenJDK.	NASA Formal Methods	2011	DBLP DOI BibTeX RDF
23	Hermann Lehner	A formal definition of JML in Coq and its application to runtime assertion checking.		2011	RDF