User Tools

Site Tools


starter_projects

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
starter_projects [2015/05/07 10:07]
pkesseli Added "Java Memory Model" section.
starter_projects [2016/01/28 14:38] (current)
mbrain Add an idea from the mailing list.
Line 231: Line 231:
  
 CBMC's Java front-end is currently in development and will support the full Java bytecode instruction set soon. Beyond that, it would be great to support some more advanced aspects of the Java programming language semantics, such as the Java Memory Model. This will include adding models for a subset of the Java concurrency packages in the Java Runtime Library. Jade Alglave may have some additional input on this. CBMC's Java front-end is currently in development and will support the full Java bytecode instruction set soon. Beyond that, it would be great to support some more advanced aspects of the Java programming language semantics, such as the Java Memory Model. This will include adding models for a subset of the Java concurrency packages in the Java Runtime Library. Jade Alglave may have some additional input on this.
 +
 +
 +==== Deadlock Analysis ====
 +
 +Michael outlined an instrumentation approach to deadlock / termination analysis [[https://​groups.google.com/​forum/#​!topic/​cprover-support/​FFrGGO1YZdQ|on the support mailing list]]. ​ It would be nice to turn this into an actual analysis.
 +
starter_projects.txt ยท Last modified: 2016/01/28 14:38 by mbrain