Verification Condition Splitting
Contents
1. If the offending path of G ends in S then it will offend Go otherwise it will offend G Conversely again both Go and Gi are subgraphs of G uint find_zero uint m requires exists uint k k lt m f k 0 ensures f result 0 for uint i 0 i lt m i invariant forall uint j j lt i f j 0 if f i 0 return i assert false assume y 30 lt k lt m f k 0 30 lt k lt m f k 0 30 lt k lt m f k 0 assert Y i x ig 0 ip 0 y Legend Y Y Y VOSj lt ip fG 0 VO lt j lt i FU 0 true Y v Yy a0 lt j lt i fO 0 30 lt j lt i fi 0 F0 lt j lt i fi 0 Y f Yy v lt m i lt m i lt m i lt m I i fli 0 a f i 0 false fli 0 a f ix 0 false Y i i Y result i i i 1 result i i 1 V0 lt j lt i fj 0 VO lt Sj lt in fi 0 Yy Y f result 0 f result 0 f result 0 Fig 0 A horizontal split 3 The Right Split To choose a horizontal split we estimate the cost complexity of a VC and then take square of the cost to crudely estimate the time the SMT solver will take to check the VC We choose the horizontal split where the sum of estimated times of resulting VCs is minimal Th2. 40 50 60 80 100 140 180 Executelnstruction Executelnstruction scaled 300 PTT IUOTITIOOTITIVIIIITTII RE T e 80 ETET FITEIIFIEITEITETIITE IETA 250 J4 70 60 50 f 40 30 20 ae reer 10 STOTT TT itis QO LLLLL Li 4 6 810 20 40 55 80 120 200 400 800 1200 4 6 810 20 40 55 80 120 200 400 800 1200 Fig 2 Runtime versus yz for two functions upper left plot and runtime versus number of splits the rest 3 1 To Split Or Not To Split We offer two modes of operation of the splitting procedure static and dynamic splitting In static splitting the user specifies the number of splits to be generated We start with a single input CFG Then we repeatedly split the CFG with largest estimated cost until we either reach the limit of splits or splitting is no longer possible In dynamic mode of operation we run the theorem prover for seconds on a VC generated from the given CFG and if it timeouts we try to split the CFG into k pieces We distinguish two values of t one is for ordinary tries defaults to one second and the other one defaults to half a minute is for last resort calls Such a last resort call is one where the VC is generated from a CFG with just a single assert on a single path and therefore cannot be split any further The parameter k is also configurable with reasonable values between 2 and 50 3 2 Error Reporting And Progress Information The error reports are usually constructed from model
3. VC splitting technique reintroduces this program structure VC generators that use interactive or resolution based theorem provers as back ends like the Why tool 8 usually split the VC completely i e down to one path and one assertion before going to the prover The Why tool even allows for further splitting This is understandable as resolution is known not to handle case splits very efficiently and for interactive provers reducing the size of the formula is essential for the human being to understand it However because SMT solvers use rather different search strategy than the resolution based theorem provers they are particularly good at exploiting Boolean structure of the formula It is only the interaction with quantifier instantiation that sometimes causes them to fail indeed both our experimental data and 10 show that introducing too many splits slows down the verification process Our approach is therefore a middle ground between what Boogie used to do thus avoiding exponential explosion in the number of paths and what the Why tool does thus providing better error reporting progress information and scalability in some cases Future Work It is likely that splitting inside the SMT solver would be more effective Let us call the CFG nodes where the splitting algorithm would perform a split special Special CFG nodes correspond to special abstract syntax tree nodes in the VC Special nodes in the VC correspond to special Boolean li
4. 0 60 RtlpZeroPages RtlpZeroSinglePage 160 ar N Ce 160 ip Pisa 140 L J 140 A 4 120 4 120 4 100 j 80 60 40 20 et ca ae fear Pde 123 4 5 6 7 8 9 10 60 Fig 5 Functions from ht list c and Vx86 time versus number of splits show it is possible to formulate VCs in a way that in practice often allow the prover to discharge a proof obligation once and for all even if proof obligation occurs along exponentially many program paths 10 As a simple illustrative example consider a procedure p of the form T p ensures result null T t new T return t 12 If the elided code does not contain other return statements and does not update the local variable t then the postcondition follows directly regardless of how many execution paths go through the elided code Patterns like these occur often enough in code that it is worthwhile and for ESC Java essential 10 to structure the VC in a way that allows the theorem prover to attempt the proof without having to do it once for each execution path leading to the return statement Based on this insight Boogie implemented an even more advanced encoding of unstructured programs 4 However as evidence from numerous verification efforts has shown the resulting flat structure provides often too little guidance about a good order in which to do case splits And even lemma learning SAT solvers cannot always overcome this problem Our
5. PLDI 2002 pages 234 245 2002 Cormac Flanagan and James B Saxe Avoiding exponential explosion Generating com pact verification conditions In Conference Record of the 28th Annual ACM Symposium on Principles of Programming Languages pages 193 205 ACM January 2001 Yuri Gurevich and Charles Wallace Specification and verification of the windows card runtime environment using abstract state machines Technical Report MSR TR 99 07 Mi crosoft Research 1999 D C Luckham S M German F W von Henke R A Karp P W Milne D C Oppen W Polak and W L Scherlis Stanford Pascal Verifier user manual Technical Report STAN CS 79 731 Stanford University 1979 Stefan Maus Michal Moskal and Wolfram Schulte Vx86 x86 assembler simulated in c powered by automated theorem proving In Jos Meseguer and Grigore Rosu editors AMAST volume 5140 of Lecture Notes in Computer Science pages 284 298 Springer 2008 D L Parnas A technique for software module specification with examples Communications of the ACM 15 5 330 336 May 1972 14
6. Verification Condition Splitting K Rustan M Leino Micha Moskal and Wolfram Schulte Microsoft Research Redmond WA USA leino schulte microsoft com 1 University of Wroc aw Poland and European Microsoft Innovation Center Aachen Germany michal moskal microsoft com Manuscript KRML 192 10 October 2008 Abstract In a traditional approach to program verification the correctness of each procedure of a given program is encoded as a logical formula called the verification condition It is then up to a theorem prover like an automatic SMT solver to analyze the verification condition in the attempt to either establish the validity of the formula thus proving the correct correct or find counterexamples thus revealing errors in the program This paper presents a technique that via program structure aware transformations that split one verification condition up into several lead to better overall performance of the SMT solver sometimes making it up to several orders of magnitude faster The technique also lends itself to improved error messages in case of verification failure due to time outs 0 Introduction Verification condition generation offers a straightforward way to harness the power of a theorem prover in program verification first encode the program s correctness con ditions as a logical formula called the verification condition VC and then use the theorem prover to analyze this formula If the theorem pro
7. aby Hypervisor 2 a min imal implementation of CPU simulator along with a virtualization layer Due to com plex functional specifications some medium size functions were difficult to impossible to handle without splitting the handle_illegal from Fig 2 comes from the Baby Hypervisor as do all functions from Fig 3 Examples of functions where splitting really helps or even makes the verification possible are handle_illegal handle_movi2s and hv_dispatch In some other cases it reduces randomness while for example in update_spt is useless which is why we allow the user to specify the needed amount of splitting The Fig 2 also gives comparison of using different values of yg for two functions We have chosen small non optimal number of splits in both cases because only then the changes in yg have noticeable effects A side note the closer we go to one path 10 Executelnstruction 10 splits Executelnstruction 15 splits 250 i l 160 140 L p 120 a 100 i 4 0 5 0 9 1 1 1 3 1 5 1 7 1 8 1 9 handle_reset 40 splits 30 Fig 4 Runtime versus yz one assertion per theorem prover call the less choice of split and in turn cost com putation influences the proving process This is especially true when doing dynamic splitting The default value of yz is 0 5 which forces horizontal splitting as long as possi ble before resorting to vertical splitting The reason is that horizon
8. by adding additional two exit nodes labeled with assume true A horizontal split of a CFG G V E e L is created by choosing a node n with two exits no and ny i e no A n n 4 no and n F no and creating two CFGs Go and G4 such that Vo R E n m V R E n no e Go Vo EN Vo x Vo e L Gy Vi ENA Vi x V1 e Ll R E m That is for Go we remove n z n and every nodes that become unreachable and for G we remove n z n and every nodes that become unreachable as well as all assert nodes above n We show an example of a horizontal split of the CFG in Fig 0 Theorem 1 Horizontal split of G into Go and G is correct Proof If G goes wrong then consider its offending path and model 0 If the path contains edge n n then it does not contain n no the graph is acyclic so the path is also present in G1 The last node on the path is reachable from n thus the assert is still present in L R n Therefore the same path and model will offend G4 1 Otherwise as the edge n n is not used the path is present in Go The final assert is untouched we do not cut the labelling function for Go and thus the path and model will offend Go Conversely both Go and G are subgraphs of G in the sense of Lemma 3 Fora set S C V the vertical split of CFG G V E e L is Go V E e L g G V E e Livs Theorem 2 Vertical split of G into Go and G is correct Proof
9. e split to occur at n17 because the alternative of chopping just ng is unlikely assume y no ng ni6 PET lat Tal Tol E n n2 n7 ng n 7 N18 Ye 0 4 Y Yy A pr SME ye 0 8 nz no nig N20 e Re FO Yy i n4 ns nio n n21 v n z ni3 n22 Nig N45 gees Fig 1 Example control flow graphs preferred horizontal splits are marked to simplify the CFG a lot whereas reducing the number of paths leading to n and onward might If yg 0 5 the number of prover paths at each node will be 1 therefore the best horizontal splits will be at n3 ng because both significantly reduce number of assert nodes in subproblems and at n1 because other splits will duplicate several asserts in both subproblems We therefore fail because the algorithm cannot see that reducing the number of paths leading to nz might be better than chopping nig If yz 1 0 we consider all CFG paths to be prover paths therefore there is no difference between no and ng we always get symmetrical subproblems either with two asserts and one path leading to each or with one assert and two paths leading to it however in the scaled up version we split at ng this split reduces the cost by half while the other creates inequality by placing n7 and ng in one of th
10. e square will also lead to preference of splits that generate roughly equal VCs Let Kz T R be a function assigning the estimated cost of checking satisfiabil ity of a formula This can depend on for example the size of a formula or the subset of signature used Our current implementation however just takes the cost to be constant Let Kain d ET when assert 7 c l yc Kr w when l assume y The intuition behind y which defaults to 0 01 in our implementation is that the assert nodes are the ones that need to be proven however adding additional possi bly irrelevant assume y nodes confuses the prover and also takes some time When proving a node the prover will likely separately consider most of the paths leading to the node However it might not need to consider them all if it finds out that the assumptions on them are irrelevant We therefore estimate the number of prover paths with the Kg V R function 1 when n e Keln when there is only one n such that n z K a n JE 5 Keg n otherwise ngn where yp defaults to 0 8 is the coefficient estimating how the prover learns from one path when processing another When yg 1 then the number of prover paths equals the number of CFG paths or in other words we assume the prover does not learn anything The cost of a node Ky V R is Ky n Ke L n Yv Keln where yy defaults to 1 0 is meant to model the fact that th
11. e subproblems failing the opportunity to first greatly reduce number of asserts If yz is somewhere between the two extremes e g 0 8 the default choice we do all three splits correctly This is further motivated by experimental data see Section 4 especially Fig 2 3 0 Complexity Computing the cost of a CFG is a linear operation therefore finding an optimal hori zontal split can be done in quadratic time by checking all possible horizontal splits Considerable performance gains can however be obtained by grouping chains of nodes into super nodes The cost of such a super node can be computed once and the edges inside of it need not be considered when splitting horizontally Therefore choos ing the optimal split becomes linear in the size of CFG and quadratic in the number of nodes with two exits which is usually considerably smaller and seems to work fine in practice i e we have never found the splitting time to be significant when compared to the time spent in the SMT solver However note that if ye 1 then the assert and assume costs of a super node needs to be kept separately since we might want to compute the cost of a CFG when asserts are turned into assumes 400 handle_illegal 1200 TPFIrir rrigv rigrirrirrivg grgggyTt p T T Ta Executelnstruction 6 splits 350 handle_illegal 20 splits 1000 1 0 ELI y t E S 1 5 0 6 0 7 0 8 0 9 1 5678910 15 30
12. eory i e p T the notion M F means the formula is true in model M The procedure is presented as control flow graph CFG which is a quadruple G V E e L where V is finite set of vertices C V x V is the set of edges e V is the entry point and L V C is the labelling function The set of labels is defined as L assume assert We use the notion Mona for no n E Let 5 be the smallest transitive relation containing a and ts smallest reflexive relation containing Let R E n be the set of nodes reachable from n i e n R E n iff n n We put the following requirements on CFGs acyclicity i e there does not exist n E V such that n tn all vertices should be reachable from entry i e V R E e it follows that there are no edges ending in e The set of all CFGs is denoted G For a given G G where G V FE e L we define _ fo when L n assume conde true otherwise true when n e preg n V nt on Pleg n A condg n otherwise E ee ee preg n when L n assert false otherwise wrong G V cy wrong n We say the program represented by a CFG G goes wrong iff there exists a model M such that M wrong G We imagine that M represents an execution trace pre q is the condition that execution trace has to fulfil at the entry of the node and wrong lt is the condition saying that the assertion fails in given execution t
13. ere might be some constant cost of proving the formula irrespective of the number of paths The cost of a CFG is just a sum of costs of all nodes in it Kg G Kv v vEeV The only vertical split we consider is the one that assigns the first half in DFS search order of asserts to one CFG and the second half to the other Let us consider splits of a CFG G where the best horizontal split results in Go and G and the vertical split results in Gg and G3 We will choose the horizontal split if Kg G lt yx Kg Go Kg G1 and vertical split otherwise The default choice of yg 0 5 prefers horizontal splits it only resorts to vertical splitting when we have a single path Motivation for choice of coefficients For a moment let us assume yc 0 it is close to zero anyhow and yg 0 for larger CFGs the path cost will dominate The cost of a CFG is now the sum over number of prover paths leading to each assertion Consider CFGs from Fig 1 The objective of a split is to get two CFGs that are simpler for the prover We would like the first CFG to be split at ng because it will give us two roughly equal subproblems and not at no because it is unknown if the case split will affect reasoning below ng The split of the second CFG should also be done in the deeper ng node as this CFG is just a scaled up version of the previous one that is most of reasoning will likely happen near the leafs not in the case split Lastly we want th
14. milliseconds not days In this paper we explore a way to reduce the time taken to verify each procedure Our general idea is to split the verification condition of a procedure into several verification conditions whose conjunction is equivalent to the original one Ideally a theorem prover would be able to prove a formula in the same time that it takes it to prove and w separately In fact it is not outrageous to think the prover could prove A w faster than and w separately because proving one conjunct may lead to the discovery of lemmas that are useful in the proof of the other However we have observed that while in most cases proving A together takes less time then proving them separately it is sometimes the case that the SMT solver can prove each of and Y ina very short time but proving A can be orders of magnitude slower Our observed phenomenon is particularly pronounced for larger VCs It is hard to pinpoint the exact cause for such crosstalk even with the help of the authors of the SMT solver but one can speculate that for example the conjunction gives rise to unfruitful quantifier instantiations that in turn lead to a plethora of new case splits More specifically our idea is to split VCs using control flow information This may be a win over more arbitrary formula splitting if for example the lemmas discovered during the proof of one proof obligation turn out to be useful also for other proof obliga
15. ntroduced one function per virtual machine in struction This approach was so successful that we decided to automate it The results of applying automatically different number of splits to the ExecuteInstruction are given in Fig 2 Applying 4 splits took up to 300 seconds trying 3 or less including no splitting would not finish in one day However going to 10 or more splits will con sistently bring the verification time into the reasonable 20 second range We can also observe that introducing more splits significantly reduces differences due to random seeds which is expected as we are processing several independent formulas handle_movi2s hv_dispatch 140 120 100 80 60 40 20 1 1 345811 17 2 35 45 60 80 100 2345811 17 25 35 45 60 80 100 handle_pf handle_reset 200 ea a ae Fe De Te aa SP a a E Si 70 Pat ae OT Patt pal ea PE 180 160 140 120 100 i DELAS UER SOS Cr Ce Ex SCT EA A Ce SRY EW Co 1 Y I e 2345811 17 25 35 45 60 80 100 12345811 17 25 35 45 60 80 100 reset_guest update_spt 80 a i a a a Pal had af ol hed 16 toa oho al hol ha 70 4 14 60 4 12 50 4 10 40 H 4 8K 30 6 20 4 10 2 4 0 an Os ee A 1 1 1 0 e p aag epi ge PM i g g a pe CN NY pea 12345811 17 25 35 45 60 80 100 12345811 17 25 35 45 60 80 100 Fig 3 Baby Hypervisor functions time versus number of splits The next useful testcase for automated splitting is the B
16. race The execution trace also includes the path that lead to a failed assertion This intuition is captured by the following lemmas Let pteg n VV condg no A A condg ng 1 e no ni gt N 5N E E E Lemma 1 For every n V such that n 4 e M F preg n iff M F pte gln Proof By induction on the length of the longest path from e to n Lemma 2 For every n E V M F wrongg n iff there exists a path e no moo TN such that L n assert and M E condg no A A condg np 1 A Q For a graph G that goes wrong the path and model from Lemma 2 are called the offending path and the offending model A correct split of of a CFG G into CFGs Go and G is one where M F wrong G iff M F wrong Go V M E wrong G 2 A Split Let L be the labelling function where the asserts are only checked in S i e Hoe assume true when L n assert and n S 2 n otherwise Lemma 3 Let G V E e L and G V E e L s where V C V and E C E G is subgraph of G Any offending path and model in G will also offend G Proof Any pathin G also exists in G Moreover for every n V we have condg n conda n For the last node n on the offending path we have L s n assert and thus also L n assert We restrict ourselves to CFGs where each node has at most two exits Any CFG G can be transformed into such while preserving wrong G
17. s returned by the theorem prover However if the theorem prover times out or runs out of memory it might not give a model In case of a last resort call we can report the specific assertion to the user with a special warning about the additional incompleteness of this result Additionally because we call the theorem prover multiple times and we have the estimated costs of each call we can provide the user with progress information in terms of number and cost of remaining splits Finally for machines with more than one CPU we can run several SMT solvers at once thus making verification of a single method embarrassingly parallel We have also experimented with using multiple machines for verification where VCs are distributed over the network 4 Evaluation The splitting algorithm has been implemented inside the Boogie verification system 3 Especially the dynamic splitting has shown great usefulness during the development of specifications for C programs finally we were getting some useful error messages instead of a succinct timeout answer Section 3 2 Once the code was proven to agree with specifications and the quantifiers equipped with proper hints for the theorem prover the positive effects of splitting often diminished However for certain bigger or more complicated methods splitting was still necessary even after getting everything correct The following plots show our experience with the splitting techniques graphicall
18. tal splitting is more efficient especially in procedures with big control flow graphs The results with differ ent yy are shown in Fig 4 The intuition is that horizontal splitting makes the formula smaller and thus simpler while vertical splitting just divides the asserts There are also examples of the aforementioned behavior where the splitting esp the dynamic splitting was necessary during development but the final specification no longer needs it One such example is the ht list c an implementation of a doubly linked list with a specification covering full functional correctness another are some functions resulting from Vx86 x86 assembly code verification 13 Introducing a couple splits helps a bit with the average time and significantly reduces differences due to random seeds Introducing too many splits slows the verification process down considerably and in case of Vx86 also makes the verification times more random 5 Related and Future Work There are many potential benefits to giving the theorem prover the entire verification condition for each procedure For example Flanagan and Saxe report numbers that 11 InsertHeadList 25 1 InsertTailList 1 i 1 i 1 123 4 5 67 8 9 10 RemoveEntryList 12 I ee 123 45 6 7 8 9 10 20 40 RemoveHeadList 12 T 1 2b 4 2h 4 0 1 0 1 123 45 6 7 8 9 10 20 40 60 123 45 6 7 8 9 10 20 4
19. terals in the CNF translation For the SMT solver splitting amounts to bumping activity of the special literals and cleaning up the set of conflict clauses when backtracking through special literals Implementing such a strategy will require significant effort and unfortunately needs to be redone for each SMT solver 6 Conclusions We have presented a method splitting verification conditions based on control flow We have proven the method correct and shown how it can be applied to bring enormous speedups in some cases compared to a monolithic VC The method also bridges the gap between the full VC splitting employed in some other verification systems and the monolithic VC References 0 The HAVOC property checker 2008 http research microsoft com projects havoc 13 10 11 12 13 14 Verifing C Compiler 2008 Soon to be available at http research microsoft com Eyad Alkassar and Wolfgang Paul On the verification of a baby hypervisor for a RISC machine draft 0 January 2008 http www wjp cs uni sb de lehre vorlesung rechnerarchitektur ws0607 layouts hypervisor pdf Mike Barnett Bor Yuh Evan Chang Robert DeLine Bart Jacobs and K Rustan M Leino Boogie A modular reusable verifier for object oriented programs In Frank S de Boer Marcello M Bonsangue Susanne Graf and Willem Paul de Roever editors Formal Methods for Components and Objects 4th International Symposium FMCO 2005
20. tions in the same branch of the program Because we want to use control flow informa tion we perform the splitting already at the level of the intermediate representation of the program before the logical formula has been generated and passed to the theorem prover The correctness of our technique which we establish in Section 2 hinges on the fact that the union of the execution traces of the split procedure equals the execution traces of the original procedure We have implemented our technique in the Boogie verification system 3 which is used as the underlying proof engine for several program verifiers including the Spec verifier and verifiers for C Havoc 0 and VCC 1 Our technique improves perfor mance in some cases up to several orders of magnitude see Section 4 Furthermore our technique allows us to output improved error messages in case of verification failure due to time outs The contributions of this paper are thus a formalization of the VC split concept along with soundness and completeness proof Sect 2 heuristical methods that specify how to choose a split and when to split Sect 3 a detailed performance evaluation of VC splitting Sect 4 1 Definitions We assume the existence of a theory used to interpret verification conditions The lan guage 7 of the theory is assumed to be closed under boolean connectives with the usual interpretations The meta variables y and refer to formulas of the th
21. ver can establish the validity of the formula then it has proven the program correct if it finds a counterexample to the given formula then it has discovered an error in the program if the theorem prover runs out of steam for example by exhausting its search strategies or reaching some resource limit then the program verifier reports an inconclusive result possibly in the form of a spurious error message This general architecture has been the basis for many program verifiers for example the Stanford Pascal Verifier 12 and the Extended Static Checker for Modula 3 7 and Java 9 To support modular verification the process of VC generation is applied separately to each part of the program traditionally at the level of each procedure cf 14 A wel come consequence thereof is that it makes program verification linear in terms of time and other resources consumed in the number of procedures in the program Unfortu nately each procedure can take a long time to verify During our work with verifying Spec 3 5 and C 1 code we have found numerous methods where the current state of the art SMT solver 6 took very long i e hours up to what would have been days to come back with an answer The usual cycle of developing verified code involves it erative calls to the program verifier intermixed with slight changes in specifications or code For this cycle to be effective we need verification times measured in minutes or preferably
22. volume 4111 of Lecture Notes in Computer Science pages 364 387 Springer September 2006 Mike Barnett and K Rustan M Leino Weakest precondition of unstructured programs In Michael D Ernst and Thomas P Jensen editors Proceedings of the 2005 ACM SIGPLAN SIGSOFT Workshop on Program Analysis For Software Tools and Engineering PASTE 05 pages 82 87 ACM September 2005 Mike Barnett K Rustan M Leino and Wolfram Schulte The Spec programming system An overview In Gilles Barthe Lilian Burdy Marieke Huisman Jean Louis Lanet and Tra ian Muntean editors Construction and Analysis of Safe Secure and Interoperable Smart devices CASSIS 2004 volume 3362 of Lecture Notes in Computer Science pages 49 69 Springer Verlag 2005 Leonardo de Moura and Nikolaj Bjrner Z3 An Efficient SMT Solver volume 4963 2008 of Lecture Notes in Computer Science pages 337 340 Springer Berlin April 2008 David L Detlefs K Rustan M Leino Greg Nelson and James B Saxe Extended static checking Research Report 159 Compaq Systems Research Center December 1998 Jean Christophe Filliatre Why a multi language multi prover verification tool Research Report 1366 LRI Universit Paris Sud March 2003 Cormac Flanagan K Rustan M Leino Mark Lillibridge Greg Nelson James B Saxe and Raymie Stata Extended static checking for Java In ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation
23. y In all plots the vertical axis gives total verification time in seconds almost all of it is spent in the prover time consumed by splitting is negligible The horizontal axis shows the influence of different parameters like number of splits or the choice of coefficients the exact parameter is given in caption of the figure All plots contain several dashed thin lines they represent runtimes of the SMT solver for the same formula but differ ent random seeds for solver s internal pseudo random number generator This is meant to accommodate for the fact that the SMT solver is highly sensitive to even minimal changes in the input formula as slight changes in the proof search grow bigger and bigger as the search progresses The bold line is arithmetical average of results All tests were performed on a 3GHz Intel machine using the Z3 6 SMT solver The test programs were translated from C using VCC 1 Our inspiration for introducing automated splitting came when we wanted to verify the C function ExecuteInstruction which essentially simulates a WindowsCard virtual machine 11 This function realizes an interpreter consisting essentially of a couple of small conditional statements followed by a big switch statement Since verifi cation of this big function 600 lines was not very responsive we initially experimented with manual splitting of this function into smaller ones for instance we introduced one function for the prelude and then we i
Download Pdf Manuals
Related Search