More Web Proxy on the site http://driver.im/

article

Preliminary design of JML: a behavioral interface specification language for java

Authors:

Gary T. Leavens,

Albert L. Baker,

Clyde RubyAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 31, Issue 3

Pages 1 - 38

https://doi.org/10.1145/1127878.1127884

Published: 01 May 2006 Publication History

Abstract

JML is a behavioral interface specification language tailored to Java(TM). Besides pre- and postconditions, it also allows assertions to be intermixed with Java code; these aid verification and debugging. JML is designed to be used by working software engineers; to do this it follows Eiffel in using Java expressions in assertions. JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch, which results in greater expressiveness. Other expressiveness advantages over Eiffel include quantifiers, specification-only variables, and frame conditions.This paper discusses the goals of JML, the overall approach, and describes the basic features of the language through examples. It is intended for readers who have some familiarity with both Java and behavioral specification using pre- and postconditions.

References

[1]

{AGH00} Ken Arnold, James Gosling, and David Holmes. The Java Programming Language Third Edition. Addison-Wesley, Reading, MA, 2000.]]

Digital Library

[2]

{Ame87} Pierre America. Inheritance and subtyping in a parallel object-oriented language. In Jean Bezivin et al., editors, ECOOP '87, European Conference on Object-Oriented Programming, Paris, France, pages 234--242, New York, NY, June 1987. Springer-Verlag. Lecture Notes in Computer Science, volume 276.]]

Digital Library

[3]

{Ame91} Pierre America. Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, REX School/Workshop, Noordwijkerhout, The Netherlands, May/June 1990, volume 489 of Lecture Notes in Computer Science, pages 60--90. Springer-Verlag, New York, NY, 1991.]]

Digital Library

[4]

{Bac88} R. J. R. Back. A calculus of refinements for program derivations. Acta Informatica, 25(6):593--624, August 1988.]]

Digital Library

[5]

{BG98} Kent Beck and Erich Gamma. Test infected: Programmers love writing tests. Java Report, 3(7):37--50, 1998.]]

[6]

{BMR95} Alex Borgida, John Mylopoulos, and Raymond Reiter. On the frame problem in procedure specifications. IEEE Transactions on Software Engineering, 21(10): 785--798, October 1995.]]

Digital Library

[7]

{BMvW98} Ralph Back, Anna Mikhajlova, and Joakim von Wright. Modeling component environments and interactive programs using iterative choice. Technical Report 200, Turku Centre for Computer Science, September 1998. http://www.tucs.abo.fi/publications/techreports/TR200.html.]]

Digital Library

[8]

{BvW98} Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.]]

Digital Library

[9]

{BW00} Martin Büchi and Wolfgang Weck. Generic wrappers. In Elisa Bertino, editor, ECOOP 2000 --- Object-Oriented Programming 14th European Conference, volume 1850 of Lecture Notes in Computer Science, pages 201--225, 2000.]]

Digital Library

[10]

{Cha02} Patrice Chalin. Back to basics: Language support and semantics of basic infinite integer types in JML and Larch. Technical Report CU-CS 2002-003.1, Computer Science Department, Concordia University, October 2002.]]

[11]

{Cha04} Patrice Chalin. JML support for primitive arbitrary precision numeric types: Definition and semantics. Journal of Object Technology, 3(6):57--79, June 2004.]]

[12]

{Che03} Yoonsik Cheon. A runtime assertion checker for the Java Modeling Language. Technical Report 03-09, Department of Computer Science, Iowa State University, Ames, IA, April 2003. The author's Ph.D. dissertation.]]

[13]

{CL02a} Yoonsik Cheon and Gary T. Leavens. A run-time assertion checker for the Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun, editors, Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada, USA, June 24-27, 2002, pages 322--328. CSREA Press, June 2002.]]

[14]

{CL02b} Yoonsik Cheon and Gary T. Leavens. A simple and practical approach to unit testing: The JML and JUnit way. In Boris Magnusson, editor, ECOOP 2002 --- Object-Oriented Programming, 16th European Conference, Máalaga, Spain, Proceedings, volume 2374 of Lecture Notes in Computer Science, pages 231--255, Berlin, June 2002. Springer-Verlag.]]

Digital Library

[15]

{CL05} Yoonsik Cheon and Gary T. Leavens. A contextual interpretation of undefinedness for runtime assertion checking. In AADEBUG 2005, Proceedings of the Sixth International Symposium on Automated and Analysis-Driven Debugging, Monterey, California, September 19--21, 2005, pages 149--157. ACM Press, September 2005.]]

Digital Library

[16]

{Coh90} Edward Cohen. Programming in the 1990s: An Introduction to the Calculation of Programs. Springer-Verlag, New York, NY, 1990.]]

Digital Library

[17]

{DL96} Krishna Kishore Dhara and Gary T. Leavens. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pages 258--267. IEEE Computer Society Press, March 1996. A corrected version is Iowa State University, Dept. of Computer Science TR #95-20c.]]

Digital Library

[18]

{ECGN01} Michael Ernst, Jake Cockrell, William G. Gris-wold, and David Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):99--123, February 2001.]]

Digital Library

[19]

{Fin96} Kate Finney. Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering, 22(2):158--159, February 1996.]]

Digital Library

[20]

{FL98} John Fitzgerald and Peter Gorm Larsen. Modelling Systems: Practical Tools in Software Development. Cambridge, Cambridge, UK, 1998.]]

[21]

{GHG+93} John V. Guttag, James J. Horning, S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, New York, NY, 1993.]]

Digital Library

[22]

{GJSB00} James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language Specification Second Edition. The Java Series. Addison-Wesley, Boston, Mass., 2000.]]

Digital Library

[23]

{GL86} David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. In ACM Conference on LISP and Functional Programming, pages 28--38. ACM, August 1986.]]

Digital Library

[24]

{GS95} David Gries and Fred B. Schneider. Avoiding the undefined by underspecification. In Jan van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, number 1000 in Lecture Notes in Computer Science, pages 366--373. Springer-Verlag, New York, NY, 1995.]]

[25]

{Hay93} I. Hayes, editor. Specification Case Studies. International Series in Computer Science. Prentice-Hall, Inc., second edition, 1993.]]

Digital Library

[26]

{Hoa69} C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--583, October 1969.]]

Digital Library

[27]

{Hoa72} C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972.]]

Digital Library

[28]

{Hui01} Marieke Huisman. Reasoning about Java Programs in higher order logic with PVS and Isabelle. Ipa dissertation series, 2001-03, University of Nijmegen, Holland, February 2001.]]

[29]

{Jon90} Cliff B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition, 1990.]]

Digital Library

[30]

{Jon91} H. B. M. Jonkers. Upgrading the pre- and postcondition technique. In S. Prehn and W. J. Toetenel, editors, VDM '91 Formal Software Development Methods 4th International Symposium of VDM Europe Noordwijkerhout, The Netherlands, Volume 1: Conference Contributions, volume 551 of Lecture Notes in Computer Science, pages 428--456. Springer-Verlag, New York, NY, October 1991.]]

Digital Library

[31]

{JvdBH+98} Bart Jacobs, Joachim van den Berg, Marieke Huisman, Martijn van Berkum, Ulrich Hensel, and Hendrik Tews. Reasoning about Java classes (preliminary report). In OOPSLA '98 Conference Proceedings, volume 33(10) of ACM SIGPLAN Notices, pages 329--340. ACM, October 1998.]]

Digital Library

[32]

{LB99} Gary T. Leavens and Albert L. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999, Proceedings, volume 1709 of Lecture Notes in Computer Science, pages 1087--1106. Springer-Verlag, 1999.]]

Digital Library

[33]

{LBR99} Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175--188. Kluwer Academic Publishers, Boston, 1999.]]

[34]

{Lea96} Gary T. Leavens. An overview of Larch/C++: Behavioral specifications for C++ modules. In Haim Kilov and William Harvey, editors, Specification of Behavioral Semantics in Object-Oriented Information Modeling, chapter 8, pages 121--142. Kluwer Academic Publishers, Boston, 1996. An extended version is TR #96-01d, Department of Computer Science, Iowa State University, Ames, Iowa, 50011.]]

[35]

{Lea97} Gary T. Leavens. Larch/C++ Reference Manual. Version 5.14. Available in ftp://ftp.cs.iastate.edu/pub/larchc+ +/lcpp.ps.gz or on the World Wide Web at the URL http://www.cs.iastate.edu/~leavens/larchc++.html, October 1997.]]

[36]

{Lea00} Gary T. Leavens. Larch frequently asked questions. Version 1.110. Available in http://www.cs.iastate.edu/~leavens/larch-faq.html, May 2000.]]

[37]

{Lei95a} K. Rustan M. Leino. A myth in the modular specification of programs. Technical Report KRML 63, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301, November 1995. Obtain from the author, at [email protected].]]

[38]

{Lei95b} K. Rustan M. Leino. Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, 1995. Available as Technical Report Caltech-CS-TR-95-03.]]

Digital Library

[39]

{Lei98} K. Rustan M. Leino. Data groups: Specifying the modification of extended state. In OOPSLA '98 Conference Proceedings, volume 33(10) of ACM SIGPLAN Notices, pages 144--153. ACM, October 1998.]]

Digital Library

[40]

{LG88} John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, Calif., pages 47--57. ACM, January 1988.]]

Digital Library

[41]

{LH94} K. Lano and H. Haughton, editors. Object-Oriented Specification Case Studies. The Object-Oriented Series. Prentice Hall, New York, NY, 1994.]]

Digital Library

[42]

{LNS00} K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC/Java user's manual. Technical note, Compaq Systems Research Center, October 2000.]]

[43]

{LPC+05} Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David R. Cok, Peter Müller, and Joseph Kiniry. JML reference manual. Department of Computer Science, Iowa State University. Available from http://www.jmlspecs.org, July 2005.]]

[44]

{LPHZ02} K. Rustan M. Leino, Arnd Poetzsch-Heffter, and Yunhong Zhou. Using data groups to specify and check side effects. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02), volume 37, 5 of SIGPLAN, pages 246--257, New York, June 17--19 2002. ACM Press.]]

Digital Library

[45]

{Luc87} John M. Lucassen. Types and effects: Towards the integration of functional and imperative programming. Technical Report TR-408, Massachusetts Institute of Technology, Laboratory for Computer Science, August 1987.]]

[46]

{LvH85} David Luckham and Friedrich W. von Henke. An overview of anna - a specification language for Ada. IEEE Software, 2(2):9--23, March 1985.]]

Digital Library

[47]

{LvHKBO87} David Luckham, Friedrich W. von Henke, Bernd Krieg-Brückner, and Olaf Owe. ANNA - A Language for Annotating Ada Programs, volume 260 of Lecture Notes in Computer Science. Springer-Verlag, New York, NY, 1987.]]

Digital Library

[48]

{LW94} Barbara Liskov and Jeannette Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811--1841, November 1994.]]

Digital Library

[49]

{LW95} Gary T. Leavens and William E. Weihl. Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica, 32(8):705--778, November 1995.]]

Digital Library

[50]

{LW97} Gary T. Leavens and Jeannette M. Wing. Protective interface specifications. In Michel Bidoit and Max Dauchet, editors, TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, volume 1214 of Lecture Notes in Computer Science, pages 520--534. Springer-Verlag, New York, NY, 1997.]]

Digital Library

[51]

{Mey92a} Bertrand Meyer. Applying "design by contract". Computer, 25(10): 40--51, October 1992.]]

Digital Library

[52]

{Mey92b} Bertrand Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, NY, 1992.]]

Digital Library

[53]

{Mey97} Bertrand Meyer. Object-oriented Software Construction. Prentice Hall, New York, NY, second edition, 1997.]]

Digital Library

[54]

{Mor94} Carroll Morgan. Programming from Specifications: Second Edition. Prentice Hall International, Hempstead, UK, 1994.]]

Digital Library

[55]

{Mül02} Peter Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of Lecture Notes in Computer Science. Springer-Verlag, 2002. The author's Ph.D. Thesis. Available from http://www.informatik.fernuni-hagen. de/import/pi5/publications.html.]]

[56]

{MV94} Carroll Morgan and Trevor Vickers, editors. On the refinement calculus. Formal approaches of computing and information technology series. Springer-Verlag, New York, NY, 1994.]]

[57]

{NNA97} H. R. Nielson, F. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In M. Dam, editor, Proceedings of the Fifth LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science. Springer-Verlag, 1997.]]

Digital Library

[58]

{Org96} International Standards Organization. Information technology -- programming languages, their environments and system software interfaces -- Vienna Development Method -- specification language -- part 1: Base language. ISO/IEC 13817-1, December 1996.]]

[59]

{ORSvH95} Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107--125, February 1995.]]

Digital Library

[60]

{OSWZ94} William F. Ogden, Murali Sitaraman, Bruce W. Weide, and Stuart H. Zweben. Part I: The RESOLVE framework and discipline --- a research synopsis. ACM SIGSOFT Software Engineering Notes, 19(4): 23--28, October 1994.]]

Digital Library

[61]

{PH97} Arnd Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, January 1997.]]

[62]

{RDF+05} Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, and Robby. Extending JML for modular specification and verification of multi-threaded programs. In Andrew P. Black, editor, ECOOP 2005 --- Object-Oriented Programming 19th European Conference, Glasgow, UK, volume 3586 of Lecture Notes in Computer Science, pages 551--576. Springer-Verlag, Berlin, July 2005.]]

Digital Library

[63]

{RL00} Clyde Ruby and Gary T. Leavens. Safely creating correct subclasses without seeing superclass code. In OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, Minneapolis, Minnesota, volume 35(10) of ACM SIGPLAN Notices, pages 208--228, October 2000.]]

Digital Library

[64]

{RL05} Arun D. Raghavan and Gary T. Leavens. Desugaring JML method specifications. Technical Report 00-03e, Iowa State University, Department of Computer Science, May 2005.]]

[65]

{Ros95} David S. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1): 19--31, January 1995.]]

Digital Library

[66]

{Spi92} J. Michael Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York, NY, second edition, 1992.]]

Digital Library

[67]

{SR05} Alexandru Salcianu and Martin Rinard. Purity and side effect analysis for java programs. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation, January 2005.]]

Digital Library

[68]

{Tan94} Yang Meng Tan. Interface language for supporting programming styles. ACM SIGPLAN Notices, 29(8):74--83, August 1994. Proceedings of the Workshop on Interface Definition Languages.]]

Digital Library

[69]

{Tan95} Yang Meng Tan. Formal Specification Techniques for Engineering Modular C Programs, volume 1 of Kluwer International Series in Software Engineering. Kluwer Academic Publishers, Boston, 1995.]]

Digital Library

[70]

{TJ94} Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation, 111(2):245--296, June 1994.]]

Digital Library

[71]

{WD96} Jim Woodcock and Jim Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science, 1996.]]

Digital Library

[72]

{Wil94} Alan Wills. Refinement in Fresco. In Lano and Houghton {LH94}, chapter 9, pages 184--201.]]

[73]

{Win83} Jeannette Marie Wing. A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science, 1983.]]

Digital Library

[74]

{Win87} Jeannette M. Wing. Writing Larch interface language specifications. ACM Transactions on Programming Languages and Systems, 9(1): 1--24, January 1987.]]

Digital Library

[75]

{Win90} Jeannette M. Wing. A specifier's introduction to formal methods. Computer, 23(9):8--24, September 1990.]]

Digital Library

[76]

{WLB00} Tim Wahls, Gary T. Leavens, and Albert L. Baker. Executing formal specifications with concurrent constraint programming. Automated Software Engineering, 7(4):315--343, December 2000.]]

Digital Library

[77]

{WR25} A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, London, second edition. edition, 1925.]]

[78]

{Wri92} Andrew K. Wright. Typing references by effect inference. In Bernd Krieg-Bruckner, editor, ESOP '92, 4th European Symposium on Programming, Rennes, France, February 1992, Proceedings, volume 582 of Lecture Notes in Computer Science, pages 473--491. Springer-Verlag, New York, NY, 1992.]]

Digital Library

Cited By

Greiner SBühlmann NOhrndorf MTsigkanos CNierstrasz OKehrer TChiba SThüm T(2024)Automated Generation of Code Contracts: Generative AI to the Rescue?Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690738(1-14)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690738
Leeson WDwyer M(2024)Algorithm Selection for Software Verification Using Graph Neural NetworksACM Transactions on Software Engineering and Methodology10.1145/363722533:3(1-36)Online publication date: 14-Mar-2024
https://dl.acm.org/doi/10.1145/3637225
Boockmann JLüttgen G(2024)On the Hunt for Invalid Objects: Exploring the Object State Space with Program Mutants2024 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER60148.2024.00078(711-716)Online publication date: 12-Mar-2024
https://doi.org/10.1109/SANER60148.2024.00078
Show More Cited By

Index Terms

Preliminary design of JML: a behavioral interface specification language for java
1. Software and its engineering
  1. Software notations and tools
    1. Context specific languages
      1. Interface definition languages
    2. System description languages
  2. Software organization and properties
    1. Software system structures
      1. Software architectures

Recommendations

Tutorial on JML, the java modeling language
ASE '07: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering

The Java Modeling Language (JML) is widely used in academic research as a common language for formal methods tools that work with Java. JML is a design by contract language that can be used to specify detailed designs of Java programs, frameworks, and ...
JML (poster session): notations and tools supporting detailed design in Java
OOPSLA '00: Addendum to the 2000 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum)

JML is a notation for specifying the detailed design of Java classes and interfaces. JML's assertions are stated using a slight extension of Java's expression syntax. This should make it easy to use. Tools for JML aid in static analysis, verification, ...
Preliminary design of a unified JML representation and software infrastructure
FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs

As a Behavioral Interface Specification Language (BISL) for Java, the Java Modeling Language (JML) is tightly coupled to the base language it enhances. Up until Java 1.4, JML kept apace with the evolution of its base language. Java 5 and subsequent ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 31, Issue 3

May 2006

171 pages

ISSN:0163-5948

DOI:10.1145/1127878

Issue’s Table of Contents

Copyright © 2006 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2006

Published in SIGSOFT Volume 31, Issue 3

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

358
Total Citations
View Citations
1,754
Total Downloads

Downloads (Last 12 months)29
Downloads (Last 6 weeks)1

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Greiner SBühlmann NOhrndorf MTsigkanos CNierstrasz OKehrer TChiba SThüm T(2024)Automated Generation of Code Contracts: Generative AI to the Rescue?Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690738(1-14)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690738
Leeson WDwyer M(2024)Algorithm Selection for Software Verification Using Graph Neural NetworksACM Transactions on Software Engineering and Methodology10.1145/363722533:3(1-36)Online publication date: 14-Mar-2024
https://dl.acm.org/doi/10.1145/3637225
Boockmann JLüttgen G(2024)On the Hunt for Invalid Objects: Exploring the Object State Space with Program Mutants2024 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER60148.2024.00078(711-716)Online publication date: 12-Mar-2024
https://doi.org/10.1109/SANER60148.2024.00078
Nilizadeh ALeavens GPăsăreanu CLe XCok D(2024)Does Going Beyond Branch Coverage Make Program Repair Tools More Reliable?2024 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST60714.2024.00033(281-292)Online publication date: 27-May-2024
https://doi.org/10.1109/ICST60714.2024.00033
Leong IBarbosa R(2024)Translating meaning representations to behavioural interface specificationsJournal of Systems and Software10.1016/j.jss.2024.112009211(112009)Online publication date: May-2024
https://doi.org/10.1016/j.jss.2024.112009
Lathouwers SHuisman M(2024)Survey of annotation generators for deductive verifiersJournal of Systems and Software10.1016/j.jss.2024.111972211(111972)Online publication date: May-2024
https://doi.org/10.1016/j.jss.2024.111972
Soares TChirica IPereira M(2024)Static and Dynamic Verification of OCaml Programs: The Gospel EcosystemLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification10.1007/978-3-031-75380-0_14(247-265)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75380-0_14
Pereira M(2024)Practical Deductive Verification of OCaml ProgramsFormal Methods10.1007/978-3-031-71177-0_29(518-542)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_29
Luo ZSiegel S(2024)Collective Contracts for Message-Passing Parallel ProgramsComputer Aided Verification10.1007/978-3-031-65630-9_3(44-68)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65630-9_3
Boockmann JLüttgen G(2024)Comprehending Object State via Dynamic Class Invariant LearningFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_7(143-164)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57259-3_7
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents