Search results for "JML"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
23	Patrice Chalin, Robby, Perry R. James, Jooyong Lee, George Karabotsos	Towards an industrial grade IVE for Java and next generation research platform for JML.	Int. J. Softw. Tools Technol. Transf.	2010	DBLP DOI BibTeX RDF
23	Lydie du Bousquet, Yves Ledru, Olivier Maury, Catherine Oriat, Jean-Louis Lanet	Reusing a JML Specification Dedicated to Verification for Testing, and Vice-Versa: Case Studies.	J. Autom. Reason.	2010	DBLP DOI BibTeX RDF
23	Frank S. de Boer, Stijn de Gouw, Jurgen J. Vinju	Prototyping a tool environment for run-time assertion checking in JML with communication histories.	FTfJP@ECOOP	2010	DBLP DOI BibTeX RDF
23	Wojciech Mostowski, Erik Poll	Midlet Navigation Graphs in JML.	SBMF	2010	DBLP DOI BibTeX RDF
23	Tanveer Mustafa, Michael Drouineaud, Karsten Sohr	Towards formal specification and verification of a role-based authorization engine using JML.	SESS@ICSE	2010	DBLP DOI BibTeX RDF
23	Faraz Hussain 0001, Gary T. Leavens	temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties.	SEFM	2010	DBLP DOI BibTeX RDF
23	Christian Murphy, Kuang Shen, Gail E. Kaiser	Using JML Runtime Assertion Checking to Automate Metamorphic Testing in Applications without Test Oracles.	ICST	2009	DBLP DOI BibTeX RDF
23	Robby, Patrice Chalin	Preliminary design of a unified JML representation and software infrastructure.	FTfJP@ECOOP	2009	DBLP DOI BibTeX RDF
23	Marieke Huisman	On the interplay between the semantics of Java's finally clauses and the JML run-time checker.	FTfJP@ECOOP	2009	DBLP DOI BibTeX RDF
23	Taekgoo Kim, Kevin Bierhoff, Jonathan Aldrich, Sungwon Kang	Typestate protocol specification in JML.	SAVCBS	2009	DBLP DOI BibTeX RDF
23	Néstor Cataño, Fernando Barraza, Daniel García, Pablo Ortega, Camilo Rueda	A Case Study in JML-Assisted Software Development.	SBMF	2008	DBLP DOI BibTeX RDF
23	Ben Yan, Masahide Nakamura, Lydie du Bousquet, Ken-ichi Matsumoto	Validating Safety for the Integrated Services of the Home Network System Using JML.	J. Inf. Process.	2008	DBLP DOI BibTeX RDF
23	Lennart Beringer, Martin Hofmann 0001	A Bytecode Logic for JML and Types.	Arch. Formal Proofs	2008	DBLP BibTeX RDF
23	Carmen Avila, Guillermo Flores, Yoonsik Cheon	A Library-Based Approach to Translating OCL Constraints to JML Assertions for Runtime Checking.	Software Engineering Research and Practice	2008	DBLP BibTeX RDF
23	Dan Jin, Zongyuan Yang	Strategies of Modeling from VDM-SL to JML.	ALPIT	2008	DBLP DOI BibTeX RDF
23	Frédéric Dadeau, Yves Ledru, Lydie du Bousquet	Measuring a Java Test Suite Coverage Using JML Specifications.	MBT	2007	DBLP DOI BibTeX RDF
23	Reiko Heckel, Marc Lohmann	Model-driven development of reactive information systems: from graph transformation rules to JML contracts.	Int. J. Softw. Tools Technol. Transf.	2007	DBLP DOI BibTeX RDF
23	Yoonsik Cheon, Carlos E. Rubio-Medrano	Random Test Data Generation for Java Classes Annotated with JML Specifications.	Software Engineering Research and Practice	2007	DBLP BibTeX RDF
23	Julien Groslambert, Jacques Julliand, Olga Kouchnarenko	JML-based verification of liveness properties on a class in isolation.	SAVCBS@FSE	2006	DBLP DOI BibTeX RDF
23	Patrice Chalin	Early detection of JML specification errors using ESC/Java2.	SAVCBS@FSE	2006	DBLP DOI BibTeX RDF
23	David R. Cok	Specifying java iterators with JML and Esc/Java2.	SAVCBS@FSE	2006	DBLP DOI BibTeX RDF
23	Peter H. Schmitt, Isabel Tonin, Claus Wonnemann, Eric Jenn, Stéphane Leriche, James J. Hunt	A case study of specification and verification using JML in an avionics application.	JTRES	2006	DBLP DOI BibTeX RDF
23	Werner Dietl, Peter Müller 0001	Universes: Lightweight Ownership for JML.	J. Object Technol.	2005	DBLP DOI BibTeX RDF
23	Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok	How the design of JML accommodates both runtime assertion checking and formal verification.	Sci. Comput. Program.	2005	DBLP DOI BibTeX RDF
23	Yoonsik Cheon, Ashaveena Perumandla	Specifying and Checking Method Call Sequences in JML.	Software Engineering Research and Practice	2005	DBLP BibTeX RDF
23	Claude Marché, Christine Paulin-Mohring, Xavier Urbain	The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML.	J. Log. Algebraic Methods Program.	2004	DBLP DOI BibTeX RDF
23	Bart Jacobs 0001	Weakest pre-condition reasoning for Java programs with JML annotations.	J. Log. Algebraic Methods Program.	2004	DBLP DOI BibTeX RDF
23	Patrice Chalin	JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics.	J. Object Technol.	2004	DBLP DOI BibTeX RDF
23	Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll	An overview of JML tools and applications.	FMICS	2003	DBLP DOI BibTeX RDF
23	Peter Müller 0001, Arnd Poetzsch-Heffter, Gary T. Leavens	Modular specification of frame properties in JML.	Concurr. Comput. Pract. Exp.	2003	DBLP DOI BibTeX RDF
23	Engelbert Hubbers, Martijn Oostdijk	Generating JML Specifications from UML State Diagrams.	FDL	2003	DBLP BibTeX RDF
23	Néstor Cataño, Marieke Huisman	CHASE: A Static Checker for JML's Assignable Clause.	VMCAI	2003	DBLP DOI BibTeX RDF
23	Erik Poll, Joachim van den Berg, Bart Jacobs 0001	Formal specification of the JavaCard API in JML: the APDU class.	Comput. Networks	2001	DBLP DOI BibTeX RDF
23	Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs 0001	JML (poster session): notations and tools supporting detailed design in Java.	OOPSLA Addendum	2000	DBLP DOI BibTeX RDF
23	Robert A. Barta, Markus W. Schranz	Syndication with JML.	SAC (2)	2000	DBLP DOI BibTeX RDF
23	Erik Poll, Joachim van den Berg, Bart Jacobs 0001	Specification of the JavaCard API in JML.	CARDIS	2000	DBLP BibTeX RDF
23	Gary T. Leavens, Albert L. Baker, Clyde Ruby	JML: A Notation for Detailed Design.	Behavioral Specifications of Businesses and Systems	1999	DBLP DOI BibTeX RDF
22	Myoung Kim, Yoonsik Cheon	A Fitness Function to Find Feasible Sequences of Method Calls for Evolutionary Testing of Object-Oriented Programs.	ICST	2008	DBLP DOI BibTeX RDF	genetic algorithms, object-oriented programming, test data generator, fitness function, evolutionary testing, pre and postconditions, JML language
14	Juan P. Galeotti, Nicolás Rosner, Carlos López Pombo, Marcelo F. Frias	Analysis of invariants for efficient bounded verification.	ISSTA	2010	DBLP DOI BibTeX RDF	dynalloy, kodkod, sat-based code analysis, static analysis, alloy
14	Christoph Lüth, Dennis Walter	Certifiable Specification and Verification of C Programs.	FM	2009	DBLP DOI BibTeX RDF
14	Joseph R. Kiniry, Fintan Fairmichael	Ensuring Consistency between Designs, Documentation, Formal Specifications, and Implementations.	CBSE	2009	DBLP DOI BibTeX RDF
14	Néstor Cataño, Camilo Rueda	Teaching Formal Methods for the Unconquered Territory.	TFM	2009	DBLP DOI BibTeX RDF
14	Lieven Desmet, Pierre Verbaeten, Wouter Joosen, Frank Piessens	Provable Protection against Web Application Vulnerabilities Related to Session Data Dependencies.	IEEE Trans. Software Eng.	2008	DBLP DOI BibTeX RDF	Security, Reliability, Data sharing, Web technologies, Security and Protection, Web-based services, Software/Program Verification
14	Michael Möller 0002, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim	Integrating a formal method into a software engineering process with UML and Java.	Formal Aspects Comput.	2008	DBLP DOI BibTeX RDF	Java, Modelling, Model checking, UML, Formal specification, CSP, Contracts, Object-Z, Runtime checking
14	Greg Dennis, Kuat Yessenov, Daniel Jackson 0001	Bounded Verification of Voting Software.	VSTTE	2008	DBLP DOI BibTeX RDF
14	Nazareno Aguirre, Marcelo F. Frias, Pablo Ponzio, Brian J. Cardiff, Juan P. Galeotti, Germán Regis	Towards Abstraction for DynAlloy Specifications.	ICFEM	2008	DBLP DOI BibTeX RDF
14	Arsenii Rudich, Ádám Darvas, Peter Müller 0001	Checking Well-Formedness of Pure-Method Specifications.	FM	2008	DBLP DOI BibTeX RDF
14	Marc Lohmann, Leonardo Mariani, Reiko Heckel	A Model-Driven Approach to Discovery, Testing and Monitoring of Web Services.	Test and Analysis of Web Services	2007	DBLP DOI BibTeX RDF
14	Yi Wang 0013, Jianjun Zhao 0001	Specifying Pointcuts in AspectJ.	COMPSAC (2)	2007	DBLP DOI BibTeX RDF
14	Patrice Chalin, Perry R. James	Non-null References by Default in Java: Alleviating the Nullity Annotation Burden.	ECOOP	2007	DBLP DOI BibTeX RDF
14	Ádám Darvas, Peter Müller 0001	Faithful mapping of model classes to mathematical structures.	SAVCBS	2007	DBLP DOI BibTeX RDF	model classes, verification, specification, abstraction, isomorphism, java modeling language
14	Gary T. Leavens, Peter Müller 0001	Information Hiding and Visibility in Interface Specifications.	ICSE	2007	DBLP DOI BibTeX RDF
14	Ben Yan, Masahide Nakamura, Lydie du Bousquet, Ken-ichi Matsumoto	Characterizing Safety of Integrated Services in Home Network System.	ICOST	2007	DBLP DOI BibTeX RDF
14	Torben Amtoft, Sruthi Bandhakavi, Anindya Banerjee 0001	A logic for information flow in object-oriented programs.	POPL	2006	DBLP DOI BibTeX RDF	information flow, confidentiality, aliasing
14	Alexandre Courbot, Mariela Pavlova, Gilles Grimaud, Jean-Jacques Vandewalle	A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods.	CARDIS	2006	DBLP DOI BibTeX RDF
14	Anduo Wang, Fei He 0001, Ming Gu 0001, Xiaoyu Song	Verifying Java Programs By Theorem Prover HOL.	COMPSAC (1)	2006	DBLP DOI BibTeX RDF
14	Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet	JACK - A Tool for Validation of Security and Behaviour of Java Applications.	FMCO	2006	DBLP DOI BibTeX RDF
14	Aleksy Schubert, Jacek Chrzaszcz	ESC/Java2 as a Tool to Ensure Security in the Source Code of Java Applications.	SET	2006	DBLP DOI BibTeX RDF
14	Greg Dennis, Felix Sheng-Ho Chang, Daniel Jackson 0001	Modular verification of code with SAT.	ISSTA	2006	DBLP DOI BibTeX RDF	formal methods, formal verification, first-order logic, SAT, software model checking, alloy
14	Marc Lohmann, Gregor Engels, Stefan Sauer 0001	Model-driven Monitoring: Generating Assertions from Visual Contracts.	ASE	2006	DBLP DOI BibTeX RDF
14	Gregor Engels, Marc Lohmann, Stefan Sauer 0001, Reiko Heckel	Model-Driven Monitoring: An Application of Graph Transformation for Design by Contract.	ICGT	2006	DBLP DOI BibTeX RDF
14	Claude Marché, Christine Paulin-Mohring	Reasoning About Java Programs with Aliasing and Frame Conditions.	TPHOLs	2005	DBLP DOI BibTeX RDF
14	David A. Naumann	Observational Purity and Encapsulation.	FASE	2005	DBLP DOI BibTeX RDF
14	Ibrahim Lokpo, Michel Babri, Gérard Padiou	Assistance for Supporting XP Test Practices in a Distributed CSCW Environment.	XP	2004	DBLP DOI BibTeX RDF	XP-programming, distributed CSCW, Unit testing
14	Michael Möller 0002, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim	Linking CSP-OZ with UML and Java: A Case Study.	IFM	2004	DBLP DOI BibTeX RDF	Java, UML, CSP, assertions, Object-Z, runtime checking
14	Michel Bidoit, Rolf Hennicker, Alexander Knapp, Hubert Baumeister	Glass-Box and Black-Box Views on Object-Oriented Specifications.	SEFM	2004	DBLP DOI BibTeX RDF
14	Lilian Burdy, Antoine Requet, Jean-Louis Lanet	Java Applet Correctness: A Developer-Oriented Approach.	FME	2003	DBLP DOI BibTeX RDF	Proof User Interface, Java, Correctness Proof
14	Sarfraz Khurshid, Darko Marinov, Daniel Jackson 0001	An analyzable annotation language.	OOPSLA	2002	DBLP DOI BibTeX RDF	alloy analyzer, alloy modeling language, compile-time analysis, specification language, java language
14	Marieke Huisman	Verification of Java's AbstractCollection Class: A Case Study.	MPC	2002	DBLP DOI BibTeX RDF
14	Cees-Bart Breunesse, Bart Jacobs 0001, Joachim van den Berg	Specifying and Verifying a Decimal Representation in Java for Smart Cards.	AMAST	2002	DBLP DOI BibTeX RDF
14	Bart Jacobs 0001, Joseph Kiniry, Martijn Warnier	Java Program Verification Challenges.	FMCO	2002	DBLP DOI BibTeX RDF
14	Hans Meijer, Erik Poll	Towards a Full Formal Specification of the JavaCard API.	E-smart	2001	DBLP DOI BibTeX RDF
14	Joachim van den Berg, Bart Jacobs 0001, Erik Poll	Formal Specification and Verification of JavaCard's Application Identifier Class.	Java Card Workshop	2000	DBLP DOI BibTeX RDF