summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Expand)AuthorAge
* Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
* VC gen for security propertiesGravatar akashlal2015-04-05
* Compute MustReach information lazily, on-demandGravatar akashlal2015-03-16
* Added MustReach information to VC genGravatar akashlal2015-03-11
* Made it produce slightly different passive commands for assignments to assump...Gravatar wuestholz2015-01-30
* Minor change to the encoding of partially verified assertions as VCGravatar wuestholz2015-01-30
* Handle timeout in refinement loopGravatar akashlal2015-01-28
* Fixed minor issue.Gravatar wuestholz2015-01-26
* Minor changeGravatar wuestholz2015-01-26
* Worked on the verification result caching (trace output).Gravatar wuestholz2015-01-26
* Worked on the verification result caching (use native support for partially v...Gravatar wuestholz2015-01-16
* Fix related to limitations in CVC4 model parsingGravatar Ally Donaldson2015-01-14
* Added a test and a todo.Gravatar wuestholz2015-01-02
* Worked on more native support for partially-verified assertions.Gravatar wuestholz2014-12-28
* Fixed a postcondition.Gravatar wuestholz2014-12-26
* Added an annotation, :split_here, for predicate statements.Gravatar Bryan Parno2014-12-16
* Merge some FixpointVC changes that got left behindGravatar Ken McMillan2014-12-08
|\
* | Optimized the VC generation for assumption variables.Gravatar wuestholz2014-12-07
* | Fixed issue in the verification result caching.Gravatar wuestholz2014-11-10
* | Worked on the verification result caching.Gravatar wuestholz2014-11-10
* | Worked on the verification result caching.Gravatar wuestholz2014-11-05
* | Worked on the verification result caching.Gravatar wuestholz2014-11-03
* | Worked on the verification result caching.Gravatar wuestholz2014-11-03
* | Fixed minor issue.Gravatar wuestholz2014-11-02
* | Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-11-02
* | Did some refactoring.Gravatar wuestholz2014-11-02
* | SI: print if a bound was reached.Gravatar akashlal2014-10-29
* | Worked on the verification result caching.Gravatar wuestholz2014-10-19
* | Worked on the verification result caching.Gravatar wuestholz2014-10-19
* | Did some refactoring.Gravatar wuestholz2014-10-18
* | Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-10-18
* | Worked on the verification result caching.Gravatar wuestholz2014-10-17
* | Worked on the verification result caching.Gravatar wuestholz2014-10-17
* | Did some refactoring.Gravatar wuestholz2014-10-16
* | Worked on the verification result caching.Gravatar wuestholz2014-10-16
* | Fix issue in verification result caching.Gravatar wuestholz2014-10-15
* | Fix issue in verification result caching.Gravatar wuestholz2014-10-15
* | Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-10-14
* | Fix issue in verification result caching for assertions without subsumption.Gravatar wuestholz2014-10-13
* | Add a todo.Gravatar wuestholz2014-10-13
| * Merge FixpointVC changes with mainlineGravatar Ken McMillan2014-10-08
|/|
| * Added "extra recursion bound" to FixedpointVC to support Corral.Gravatar Ken McMillan2014-10-08
* | MergeGravatar akashlal2014-10-01
|\ \
| * | Minor correctionsGravatar akashlal2014-10-01
* | | fixed StackOverflow in TraceCounterexample;Gravatar qadeer2014-09-30
|/ /
* | SI: VC gen with labelsGravatar akashlal2014-09-29
* | Cleanup: removed unused codeGravatar akashlal2014-09-29
* | Fix to VC genGravatar akashlal2014-09-28
* | Fix for boolVC generationGravatar akashlal2014-09-27
* | Lets have a setter for TopLevelDeclarations as wellGravatar akashlal2014-09-25