|
Abstract In this project we used Twelf to prove some simple properties of multiset formulas with cardinality constraints. We have shown previously in [2] that reasoning about multisets with cardinality constraints belongs to the NP class and since formulas can contain arbitrary boolean connectives, the problem is NP-complete. Also, an efficient decision procedure for the reasoning about multiset formulas with cardinality constraints was published in [2]. However, there were many practical challenges that we faced while applying the described decision procedure. In this project we used Twelf to prove some formulas that were too difficult to tackle with standard SMT solvers.Introduction Recently there was increasing interest for reasoning about multisets with cardinality constraints. Multisets arise in various verification tasks, for example: in bounded model checking [3] or in resource analysis of Java programs within the Mobius project [1]. Although multisets seem like a proper abstraction for container data types, their exact complexity was not known until recently [2], when it was shown that the reasoning about multisets with cardinality constraints belongs to the NP complexity class. However, although we showed that the problem is NP-complete and although there has been a large progress in solving NP-hard problems in practice, formulas that are automatically generated by our decision procedure are still beyond the reach of state-of-the-art solvers. In this project we used Twelf to prove some theorems that we initially failed to prove using current SMT solvers. To prove those theorems, we first needed to formally specify multisets. Once this specification was completed, we were able to prove several automatically generated verification condition. Although Twelf is not an automated theorem prover and all together it required lots of interaction, some of theorems were proved fairly easily and we consider this to be a success, since it was the first time that those theorems were proved differently than using a standard pen-and-paper proof. In the rest of this report we present the relevant technical aspects of the proving process. Types: Natural Numbers and Multisets There are three basic types that we use: natural numbers (nat), multisets (mset) and false (false). Natural numbers are defined inductively::
Multisets are modeled as lists of natural numbers. They are also defined inductively:
In our initial approach we tried to model multisets as list of any elements. Using such an approach we faced difficulties while defining that two elements are different. For this reason we decided to model multisets as a list of natural numbers where non-equality of two elements can be defined in a simpler and more natural way. The type false is the uninhabited type that is standardly used as a justification that some cases are impossible. Theorems: Union, Deletion and Subset We proved the following theorems about multisets: ... to be continued.... Conclusion The goal of this project was twofold: first, we tried to exploit the potential of using Twelf in verification, and second, we tried to formally verify the proofs that we had done earlier. Those proofs were done by hand and therefore they could be error-prone. Moreover, we could not be sure that they were complete and correct. Although the formal specification of those proofs was initially a tedious task, at the end we managed to make them entirely machine checkable. This way we proved the correctness of the generated verification conditions. We have also shown that Twelf can be used in verification parallel to theorem provers. Some of the formally verified theorems were tested in the first-order theorem prover SPASS+T (first-order logic enriched with arithmetic axioms) and some of the theorems were proved in the interactive theorem prover Isabelle/HOL. In both cases, we first constructed a sketch of a proof on paper and then we invoked the prover. In SPASS+T we used various lemmas to obtain the proof, while in Isabelle/HOL we used various tactics. We can conclude from this project that proof assistants and proof verifiers are equally suited for proving verification conditions, provided that the user has sufficient experience with the system he is using. References
|
|