Looking for large(r) projects that use OpenJML
Opened this issue · 3 comments
CopperEagle commented
Hey there!
I am currently working on a thread safety testing tool that allows users to specify using JML. To test, I need some classes (datastructures) that are specified using JML. Ideally, the datastructure should be concurrent, i.e. try to be thread safe.
So far, I have only really found AWS to use JML but I really do need concurrent classes. Does anyone have some examples for projects that use JML in this context?
Thanks in advance for any suggestions.
Also, thank you @davidcok and @jsinglet for your work on openJML!
davidcok commented
There are not likely to be projects that fulfill your requirements because JML does not support reasoning about concurrency.
Nor am I aware of any large public projects that use JML.
leavens commented
Hi,
I agree with what David said about concurrency and JML: it's not designed to specify or reason about concurrent Java programs.
However, you might look at the work that is being done by:
* Marieke Huisman<http://wwwhome.ewi.utwente.nl/~marieke/> and collaborators in the Formal Methods and Tools Group<http://fmt.cs.utwente.nl/> at the University of Twente, Netherlands. Before, Marieke was part of the Everest<http://www-sop.inria.fr/everest> team at INRIA Sophia-Antipolis, that developed the JACK: Java Applet Correctness Kit<http://www-sop.inria.fr/everest/soft/Jack/jack.html> environment and the Bytecode Modeling Language (BML)<http://www.jmlspecs.org/BML>, a bytecode variation of JML.
You might also want to look at:
* Wladimir Araujo<http://www.linkedin.com/pub/wladimir-de-lara-ara%C3%BAjo/0/160/54a>, Lionel Briand<http://squall.sce.carleton.ca/people/briand/>, and Yvan Labiche<http://www.sce.carleton.ca/faculty/labiche.html>. Concurrent Contracts for Java in JML. 19th International Symposium on Software Reliability Engineering (ISSRE), pages 37-46, November 2008.
*
Edwin Rodríguez<http://www.cis.ksu.edu/~edwin/>, Matthew B. Dwyer<http://www.cis.ksu.edu/~dwyer/>, Cormac Flanagan<http://www.soe.ucsc.edu/~cormac/>, John Hatcliff<http://www.cis.ksu.edu/~hatcliff/>, Gary T. Leavens<http://www.eecs.ucf.edu/~leavens/index.html>, Robby<http://www.cis.ksu.edu/~robby/>. Extending JML for Modular Specification and Verification of Multi-Threaded Programs. In Andrew P. Black (ed.), ECOOP<http://www.ecoop.org/> <http://www.ecoop.org/> 2005 -- Object-Oriented Programming 19th European Conference, Glasgow, UK, pages 551-576. Volume 3586 of <http://www.springer.de/comp/lncs/index.html>
Lecture Notes in Computer Science<http://www.springer.de/comp/lncs/index.html>
<http://www.springer.de/comp/lncs/index.html>, Springer Verlag<http://www.springer.de/>, July 2005. The original publication is available at springerlink.com<http://www.springerlink.com/> or directly from http://dx.doi.org/10.1007/11531142_24. Also Kansas State University, Department of Computing and Information Sciences, Technical Report, SAnToS-TR2004-10, December 2004, revised May 2005. [PDF]<http://spex.projects.cis.ksu.edu/papers/SAnToS-TR2004-10.pdf>
Regards,
Gary T. Leavens
329 L3Harris Center
Computer Science, University of Central Florida
4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758
***@***.******@***.***>
…________________________________
From: CopperEagle ***@***.***>
Sent: Friday, June 28, 2024 12:42 PM
To: OpenJML/OpenJML ***@***.***>
Cc: Subscribed ***@***.***>
Subject: [OpenJML/OpenJML] Looking for large(r) projects that use JML (Issue #822)
Hey there!
I am currently working on a thread safety testing tool that allows users to specify using JML. To test, I need some classes (datastructures) that are specified using JML. Ideally, the datastructure should be concurrent, i.e. try to be thread safe.
So far, I have only really found AWS<https://github.com/aws/aws-encryption-sdk-java> to use JML but I really do need concurrent classes. Does anyone have some examples for projects that use JML in this context?
Thanks in advance for any suggestions.
Also, thank you @davidcok<https://github.com/davidcok> and @jsinglet<https://github.com/jsinglet> for your work on openJML!
—
Reply to this email directly, view it on GitHub<#822>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AC53NPOT3YHYLLCRQ5MEWG3ZJWG5ZAVCNFSM6AAAAABKCGZWROVHI2DSMVQWIX3LMV43ASLTON2WKOZSGM4DANZZGY4TSMQ>.
You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>
CopperEagle commented