Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  Ada d29fbec5 over 2 years Lélio Brun working version for stateful contracts
  C 89fd79f0 over 2 years Lélio Brun a working version for automata with 'last' case...
  EMF dccec723 over 2 years Lélio Brun a version that almost work for the k-inuctive t...
  Horn d29fbec5 over 2 years Lélio Brun working version for stateful contracts
  Java d978c46e almost 3 years Lélio Brun start instrumenting the main C function
  VHDL d978c46e almost 3 years Lélio Brun start instrumenting the main C function
backends.ml 1.17 KB d29fbec5 over 2 years Lélio Brun working version for stateful contracts
backends.mli 149 Bytes cc852504 almost 3 years Lélio Brun comment dead code with (* XXX: UNUSED *) discla...

Latest revisions

# Date Author Comment
89fd79f0 09/27/2021 06:00 PM Lélio Brun

a working version for automata with 'last' case of enums as default case

d29fbec5 09/27/2021 01:36 PM Lélio Brun

working version for stateful contracts

4fef1a04 09/23/2021 05:51 PM Lélio Brun

proper generation of stateful contracts

478edbed 09/23/2021 04:40 PM Lélio Brun

proper handling of stateless nodes and automata

0988cb68 09/23/2021 03:40 PM Lélio Brun

proper inductive case and no code generated for contracts

e164af45 09/21/2021 11:23 AM Lélio Brun

working version with additional asserts to make the axiom work

dccec723 09/20/2021 06:46 PM Lélio Brun

a version that almost work for the k-inuctive two_counters example

f51926b8 09/07/2021 04:10 PM Lélio Brun

no need to reschedule in order to "clock-protect" the unitialized state variables in ACSL !

70710795 08/25/2021 12:00 PM Lélio Brun

first draft with translated cocospec

5b98398a 07/29/2021 04:02 PM Lélio Brun

first version working with stateless contracts

View revisions

Also available in: Atom