summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/StratifiedVC.cs
Commit message (Expand)AuthorAge
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
* BlockSeq: farewellGravatar Ally Donaldson2013-07-22
* CmdSeq: farewellGravatar Ally Donaldson2013-07-22
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
* More refactoringGravatar Ally Donaldson2013-07-22
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
* mergeGravatar Pantazis Deligiannis2013-07-22
|\
| * Large refactoring of Hashtable to Dictionary.Gravatar Ally Donaldson2013-07-22
| * Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a plai...Gravatar Ally Donaldson2013-07-22
* | mergeGravatar Pantazis Deligiannis2013-07-06
|\|
| * Did some refactoring in the execution engine and worked on the parallelization.Gravatar wuestholz2013-07-01
* | merged more CVC4 and Z3 SMTLIB2 parsing methods ... results into a more compa...Gravatar pantazis2013-06-13
|/
* Parse integers returned by Z3 into BigNumGravatar akashlal2013-01-29
* Use the new ProverInterface's Evaluate method in stratified inlinigGravatar Unknown2013-01-03
* bunch of refactoringsGravatar Unknown2012-10-03
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
* deleted an unused classGravatar qadeer2012-06-12
* refactoring in SIGravatar qadeer2012-06-12
* 1. changed new SI implemnetation so that it performs substitution for call sitesGravatar qadeer2012-06-10
* final (hopefully) fix to new SIGravatar qadeer2012-06-07
* testing a fix in SIGravatar qadeer2012-06-07
* Bug fix with mvInfo during VCGenGravatar akashlal2012-06-06
* update to SIGravatar qadeer2012-06-04
* moved class Macro to AbsyGravatar qadeer2012-06-04
* added FindLeastToVerify to StratfiedVCGenBase as an abstract methodGravatar qadeer2012-05-30
* moved a couple of overrides from StratifiedVCGen to StratifiedVCGenBaseGravatar qadeer2012-05-30
* added support for recordProcCallSites to new SIGravatar qadeer2012-05-30
* extra recursion boundGravatar akashlal2012-05-30
* further refactoring of SI;Gravatar qadeer2012-05-29
* Removed program argument from VerifyImplementation. It is redundant since th...Gravatar qadeer2012-05-29
* further refactoringGravatar qadeer2012-05-28
* more refactoringGravatar qadeer2012-05-28
* MergeGravatar qadeer2012-05-28
|\
* | removed call site simplification from the old SI flowGravatar qadeer2012-05-28
| * No need for extra attributes in ExtractLoopsGravatar akashlal2012-05-28
| * updating FindLeastToVerify to the new flowGravatar akashlal2012-05-28
|/
* Better interface for adding skipped calls, andGravatar akashlal2012-05-26
* new stratified inlining (initial prototype)Gravatar qadeer2012-05-25
* more refactoring in stratified inliningGravatar qadeer2012-05-24
* small fixGravatar qadeer2012-05-21
* starting the implementation of the new stratified inlining APIGravatar qadeer2012-05-21
* MergeGravatar qadeer2012-05-10
|\
* | some other cleanupsGravatar qadeer2012-05-10
| * Slightly better management of outermost Push-Pop and FlushAxiomsGravatar Unknown2012-05-02
|/
* z3 process is killed nowGravatar qadeer2012-05-01
* added counterexample generation based on labels back to stratified inliningGravatar qadeer2012-05-01
* log file fixGravatar qadeer2012-04-30
* clean up in stratified inliningGravatar qadeer2012-04-29
* eliminated class ErrorModelGravatar qadeer2012-04-28
* removed proccopybounding codeGravatar qadeer2012-04-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 08:57:34 +0000