T-satisfiability test problem for the VL1 logical language of the VRS system

V.G. Timofeev

Abstract


In this paper we give a short introduction to the satisfiability modulo theories (SMT) problem and demonstrate how the methods developed in the SMT research field can be applied in the requirement verification tool VRS, which supports insertion modelling methodology. We formalize the logical language VL1 used for formal reasoning in VRS and justify decidability of satisfiability problem in that language. Besides we discuss the context of the problem being solved and indicate possible methods that can be used on different stages of solution. Finally, we present a satisfiable conjunction search method, which is based on a set-representation of logical connectives in formulas.

References


de Moura L., Bjørner N. Satisfiability Modulo Theories: Introduction and Applications // Communications of the ACM. –2011. – Vol. 54 (9). – P. 69–77.

The 15-th International Conference on Theory and Applications of Satisfiability Testing – Режим доступа: http://sat2012.fbk.eu

Satisfiability Modulo Theories Competition (SMMP) – Режим доступа: http://www.smtcomp.org

Letichevsky A. Algebra of behavior transformations and its applications // in V.B. Kudryavtsev and I.G. Rosenberg editors. Structural theory of Automata, Semigroups, and Universal Algebra, NATO Science Series II. Mathematics, Physics and Chemistry. – Springer. – 2005. – Vol. 207. – P. 241–272.

Letichevsky A., Kapitonova J., Kotlyarov V. et al. Insertion Modeling in Distributed System Design // Problems of Programming. – 2008. – Vol. 4. – P. 13–39.

Letichevsky A.A., Letychevskyi O.A., Peschanenko V.S. Insertion Modeling System // Lecture Notes in Computer Science. – Springer. – 2011. –Vol. 7162. – P. 262–274.

Kapitonova J., Letichevsky A., Volkov V. et al. System Validation // In R. Zurawski, editor. The Embedded Systems Handbook. – Miami: CRC Press, 2005 – P. 6.1 – 6 – 57.

.8. Letichevsky A., Kapitonova J., Letichevsky A. (jr). et al. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Computer Networks. – 2005. – N 47. – P. 662– 675.

Летичевский А.А., Капитонова Ю.В., Волков В.A. и др. Сертификация систем с помощью базовых протоколов // Кибернетика и системный анализ. – 2005. – № 4. – C. 256–268.

Letichevsky A., Gilbert D. A Model for Interaction of Agents and Environments // In D. Bert, C. Choppy, P. Moses, editors. Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science. – Springer. – 1999. – Vol. 1827. – P. 311–328.

Barrett C., Sebastiani R., Seshia S. A., Tinelli C. Satisfiability Modulo Theories // In: A. Biere, M. Heule., H. van Maaren, T. Walsh editors. Handbook of Satisfiability. – IOS Press. – 2009. – P. 737–797.

Kroening D., Strichman O. Decision Procedures – an Algorithmic Point of View. – Berlin: Springer-Verlag, 2008. – 304 p.

Davis M., Logemann G., Loveland D. Machine Program for Theorem-Proving // Comm. of the ACM. –1962. – № 5(7). – P. 7:394–397.

Ganzinger H., Hagen G., Nieuwenhuis R. et al. DPLL (T): Fast decision procedures // Proc. of the 16-th Intl. Conf. on Computer Aided Verification, Lecture Notes in Computer Science, 3114. – 2004. – P. 175–188.

de Moura L., Bjørner N. Satisfiability Modulo Theories: An Appetizer // Lecture Notes in Computer Science. –2009. – Vol. 5902. – P. 23–36.

Nelson G., Oppen D.C. Simplification by cooperating decision procedures // ACM Transactions on Programming Languages and Systems. – 1979. – Vol. 1. – P. 245–257.

Ackermann W. Solvable cases of the Decision Problem. – Amsterdam: North-Holland, 1954. – 114 p.

Dutertre B., de Moura L. Integrating Simplex with DPLL(T) // Technical report, CSL-06-01, SRI International. – 2006. – 35 p.

Weispfenning V. Mixed Real-Integer Linear Quantifier Elimination // Proceedings of the international symposium on Symbolic and algebraic computation ISSAC’99. – 1999. – P. 129–136.

Schrijver A. Theory of Linear and Integer Programming. – John Wiley & sons. – 1998. – 471 p.

Nieuwenhuis R., Oliveras R. Fast Congruence Closure and Extensions // Information and Computation. – 2007. – Vol. 205(4). – P. 557–580.


Refbacks

  • There are currently no refbacks.