[ escjava-Research-199 ] escjava3_logic

[atiti]

{{{

!html

Reply to: noreply@sort.ucd.ie }}} {{{ Research item #199, was opened at 2005-10-27 16:50 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=780&aid=199&group_id=97

Category: Theory Group: None

Status: Closed Resolution: Out of Date Priority: 3 Submitted By: Joseph Kiniry (jkiniry) Assigned to: Nobody (None) Summary: escjava3_logic

Initial Comment: A new logic called escjava3_logic, located in ESCTools/docs/Escjava2-Logics/pvs has been outlined in PVS. This new logic has an explicit heap model, new types to clearly represent concepts vital to ESC (inspired and informed by escjava2_logic), and is meant to heavily leverage the capabilities of each theorem prover in which it is embedded.

The purpose of this project is to finish writing this logic and write a VC generator for it, using Clement's new escjava.vcGeneration package as a backend, and preferably David's new JML3 as a front-end.

---

You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=780&aid=199&group_id=97 }}}

[atiti]

From: (GH: None) Date: Sat Dec 15 17:23:20 2007

added mailto line

This message has 0 attachment(s)

[atiti]

From: None (GH: None) Date: Tue Apr 27 14:34:16 2010

Milestone ESCJava2 2.0.9 release deleted