summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
Commit message (Expand)AuthorAge
* a bug fixGravatar qadeer2012-06-19
* another edit for predicationGravatar qadeer2012-06-19
* integrating predicationGravatar qadeer2012-06-19
* Removed program argument from VerifyImplementation. It is redundant since th...Gravatar qadeer2012-05-29
* more refactoringGravatar qadeer2012-05-28
* starting the implementation of the new stratified inlining APIGravatar qadeer2012-05-21
* some other cleanupsGravatar qadeer2012-05-10
* eliminated class ErrorModelGravatar qadeer2012-04-28
* removed lazy inliningGravatar qadeer2012-04-28
* various changes for using unsat cores in HoudiniGravatar qadeer2012-04-17
* further fixesGravatar qadeer2012-02-28
* various cleanup regarding /doNotUseLabelsGravatar qadeer2012-02-28
* fixing stratified inlining to deal with new path infoGravatar qadeer2012-02-27
* various fixes related to new error tracesGravatar qadeer2012-02-27
* further fixes related to using uninterpreted function for error tracesGravatar qadeer2012-02-25
* using model instead of labelsGravatar Unknown2012-02-23
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
* Boogie: fixed proof-obligation countingGravatar Rustan Leino2012-01-09
* Boogie: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* Boogie: Fixed a crash due to old expressions in lambda expressions that were ...Gravatar wuestholz2011-12-02
* Remove invariant that was just wrongGravatar Michal Moskal2011-11-28
* refactoring houdini so that it creates only a single instance of z3Gravatar qadeer2011-11-16
* Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...Gravatar Rustan Leino2011-11-15
* partial check in regarding getting states working with stratified inliningGravatar qadeer2011-09-06
* reverting irreducible handling temporarilyGravatar qadeer2011-08-21
|\
* | added code to handle irreducible graphsGravatar qadeer2011-08-20
* | minor refactoringGravatar qadeer2011-08-17
* | deleted lazyinlining option 2 and 3Gravatar qadeer2011-08-17
* | Added "procedure-copy bounding" for lazy inliningGravatar Unknown2011-08-10
* | further changes for making houdini workGravatar qadeer2011-08-04
|/
* ported all the counterexample code to Michal's new Model class; the goal is t...Gravatar Unknown2011-06-27
* early clearing of live variables and incarnation mapsGravatar qadeer2011-06-24
* implementation of iterative LetVCGravatar qadeer2011-06-23
* Bug fix for trace generation with extractLoop optionGravatar Unknown2011-06-23
* LetVC can get null label2absy from lazy inlining. So, I weakened the precond...Gravatar qadeer2011-05-03
* modified letvc generation so that the use of control flow function and labels...Gravatar qadeer2011-04-15
* added reachability information to the VC and used that to support arbitrary a...Gravatar Unknown2011-04-14
* minor fix with loopy counterexample generationGravatar akashlal2011-03-18
* new algorithm for dead code detection (vc:doomed)Gravatar schaef2011-03-15
* Replaced all dictionaries that mapped to bool (i.e., were being used to imple...Gravatar mikebarnett2011-03-10
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...Gravatar mikebarnett2011-03-10
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
* Don't treat "Inconclusive" answer as fatal when splitting.Gravatar MichalMoskal2011-02-02
* Add new feature: {:selective_checking} on procedures. See testcase for a desc...Gravatar MichalMoskal2010-12-17
* Add functions generated in lambda-expansion of function body to top-level pro...Gravatar MichalMoskal2010-12-17
* Refactoring: pulled out all code for stratified inlining to a new file.Gravatar akashlal2010-11-23
* Changed stratified inlining: can now be user-guidedGravatar akashlal2010-11-22
* Minor updates for printing coverage graph of stratified inliningGravatar akashlal2010-11-14
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
* Boogie:Gravatar rustanleino2010-10-12