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 |
|