summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* First implementation of resetting transitions.Alex Auvolat2014-07-045-40/+83
* Use LAST instead of NEXT (only EDD implementation works at the moment)Alex Auvolat2014-07-048-173/+189
* Simplifications && preparation for restart.Alex Auvolat2014-07-044-9/+35
* Changes to parser ; EDD optimisations ; test cases.Alex Auvolat2014-07-038-126/+2240
* Add ABRO example ; correct interpret bug.Alex Auvolat2014-07-038-7010/+205
* Fix some tests.Alex Auvolat2014-07-035-6/+37
* New algorithm for variable ordering based on FORCE.Alex Auvolat2014-07-032-8/+86
* Add message when a step goes on BOT, ie. contradiction in assumes.Alex Auvolat2014-07-022-25/+38
* Fix non-termination issue in EDDsAlex Auvolat2014-07-023-75/+130
* More verbosity ; adapt rfollow so that it can be provedAlex Auvolat2014-07-025-6/+23
* Small changes in Graphwiz export : same vars at same level.Alex Auvolat2014-07-011-0/+11
* Adapt for real type with Apron ; not very efficient ATM.Alex Auvolat2014-07-0117-81/+8290
* Not much : find acceptably good ordering for variables.Alex Auvolat2014-07-011-55/+28
* Finish up EDDsAlex Auvolat2014-07-014-44/+110
* Implement chaotic iterations on EDDs. Global widening is missing.Alex Auvolat2014-06-304-112/+361
* Reached interesting point in BDD implementation.Alex Auvolat2014-06-305-111/+121
* More work on EDDs.Alex Auvolat2014-06-273-159/+321
* Minor corrections.Alex Auvolat2014-06-264-4/+14
* Many things, sorry for the mess.Alex Auvolat2014-06-265-206/+615
* Implement a few things. Tomorrow: optimizations.Alex Auvolat2014-06-252-51/+138
* Begin implementation of EDD ; SCA implemented.Alex Auvolat2014-06-256-26/+536
* Differentiate pre witin different scopes.Alex Auvolat2014-06-252-0/+3
* Add command line option : verbose chaotic iterations.Alex Auvolat2014-06-252-14/+28
* Implementation of disjunction domain seems to work.Alex Auvolat2014-06-2411-547/+619
* Not much. Still does not work very well.Alex Auvolat2014-06-2011-79/+160
* Everything proved !!Alex Auvolat2014-06-194-42/+104
* Actually, it works.Alex Auvolat2014-06-193-9/+22
* Very buggy disjunction domain !Alex Auvolat2014-06-198-72/+418
* Did most of the boring stuff. Now, work on the abstract domain.Alex Auvolat2014-06-1911-109/+209
* Isolate numerical part of domain. Next: isolate numerical part of equations.Alex Auvolat2014-06-199-58/+140
* Do some typing ; support multiple pre in abstract interpretation.Alex Auvolat2014-06-199-126/+270
* Presentation changes.Alex Auvolat2014-06-181-15/+26
* Nice view of guarantees ; add half test, proved.Alex Auvolat2014-06-1811-44/+180
* RetabAlex Auvolat2014-06-182-44/+50
* Add gilbreath suite ; booleans are not represented in a good way.Alex Auvolat2014-06-1813-89/+201
* Abstract interpretation gives good results on the limiter example.Alex Auvolat2014-06-188-61/+58
* Pretty printing.Alex Auvolat2014-06-189-67/+148
* Add intervals domain ; some interesting analysis works.Alex Auvolat2014-06-188-18/+438
* Some abstract interpretation does something now.Alex Auvolat2014-06-1711-30/+205
* Add bindings to apron. Next : work on abstract interpret.Alex Auvolat2014-06-179-59/+242
* Write transformation of program into logical formula.Alex Auvolat2014-06-1710-31/+418
* Add AST for logical formula.Alex Auvolat2014-06-177-49/+123
* Implement automata and activate blocks in interpret.Alex Auvolat2014-06-164-126/+232
* Add fail updown test (using pre instead of last).Alex Auvolat2014-06-133-1/+55
* Begin of new interpret with more imperative concepts. Scope activation 'n stuff.Alex Auvolat2014-06-1311-152/+566
* Move a lot of things.Alex Auvolat2014-06-1344-153/+521
* Parse activate blocks.Alex Auvolat2014-06-137-96/+203
* Nothing.Alex Auvolat2014-06-122-5/+5
* Implement instances (that was easy!)Alex Auvolat2014-06-121-10/+15
* Adopt same output format as test.cAlex Auvolat2014-06-122-16/+39