|
|
|
Recent advances in program verification through
computer algebra |
| Lu YANG1,Chaochen ZHOU2,Naijun ZHAN2,Bican XIA3, |
| 1.Laboratory of Trustworthy
Computing, East China Normal University, Shanghai 200062, China; 2.Laboratory of Computer
Science, Institute of Software, Chinese Academy of Sciences, Beijing
100190, China; 3.LMAM & School of
Mathematical Sciences, Peking University, Beijing 100871, China; |
|
|
Harel D, Pnueli A. On the development of reactivesystems. Logics and Models of ConcurrencySystems, 1985, 13: 447–498
|
|
Lions J L. The ARIANE 5 flight 501 failure report. European Space Agency (ESA), 1996
|
|
Skeel R. Roundofferror and the Patriot missile. SIAM News, 1992, 25(4)
|
|
Reeves G, Neilson T. The mars rover spirit FLASHanomaly. In: Proceedings of IEEE AerospaceConference’05. 2005
|
|
International Conference on Verified Software:Theories, Tools and Experiments, ETH Zürich, Oct. 10–13, 2005
|
|
Queille J P, Sifakis J. Verification of concurrentsystems in CESAR. In: Proceedings of Int.Symp. On Programming. 1982, 337–351
|
|
Clarke E M, Emerson E A. Synthesis of synchronizationskeletons for branching time temporal logic. In: Proceedings of IBM Workshop on Logics of Programs. 1981, 52–71
|
|
Nipkow T, Paulson C P, Wenzel M. Tutorial on ISABELLE/HOL. Springer-Verlag, 2009
|
|
Owre S, Rushby J M, Shankar N. PVS: a protype verification system. In: Proceedings of CADE’92. 1992, 748–752
|
|
Paulin-Mohring C, Werner B. Synthesis of ML programsin the system Coq. J. Symbolic Logic, 1993, 15(5/6): 607–640
|
|
Cousot P, Cousot R. Abstraction interpretation:a unified lattice model for static analysis of programs by constructionor approximation of fixpoints. In: Proceedingsof ACM POPL’77. 1977, 238–252
|
|
Cousot P, Cousot R. Systematic design of programanalysis frameworks. In: Proceedings ofACM POPL’79. 1979, 269–282
|
|
Moszkowski B. Atemporal logic for multilevel reasoning about hardware. IEEE Computers, 1985, 18(2): 10–19
|
|
Zhou C, Hoare C A R, Ravn A. A calculus of durations. Inf.Processing Letters, 1991, 40(5): 269–276
|
|
Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 1995, 138(3): 3–34
|
|
Manna Z, Pnueli A. Verifying hybrid systems. In: Proceedings of Hybrid Systems. LNCS 736, 1993, 4–35
|
|
Lamport L. Hybridsystems in TLA+. In: Proceedings of HybridSystems. LNCS 736, 1993, 77–102
|
|
Kesten Y, Pnueli A. Timed and hybrid statechartsand their textual representation. In: Proceedingsof Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS571, 1992, 591–619
|
|
Rodriguez-Carbonell E, Kapur D. An abstract interpretationapproach for automatic generation of polynomial invariants. In: Proceedings of Static Analysis Symposium (SAS’04). 2004, 280–295
|
|
Rodriguez-Carbonell E, Kapur D. Automatic generation of polynomialloop invariants: algebraic foundations. In: Proceedings of Intl. Symp on Symbolic and Algebraic Computation (ISSAC’04). 2004
|
|
Sankaranarayanan S, Sipma H B, Manna Z. Non-linear loop invariant generation using Gröbnerbases. In: Proceedings of ACM POPL’04. 2004, 318–329
|
|
Collins G E. Quantifier elimination for real closed fields by cylindrical algebraicdecomposition. Automata Theory and FormalLanguages, LNCS 33, 1975, 134–183
|
|
Collins G E, Hong H. Partial cylindrical algebraicdecomposition for quantifier elimination. J. of Symbolic Computation, 1991, 12: 299–328
|
|
Lafferre G, Pappas G J, Yovine S. Symbolic reachability computaion for families of linearvector fields. J. of Symbolic Computation, 2001, 11: 1–23
|
|
Yang L, Zhan N, Xia B, et al. Program verification by using DISCOVERER. In: Proceedings of VSTTE’05. 2005, 575–586
|
|
Kapur D. Automaticallygenerating loop invariants using quantifier Elimination. In: Proceedings of IMACS Intl. Conf. on Applicationsof Computer Algebra (ACA’04). 2004
|
|
Henzinger T A, Wong-Toi H. Linear phase-portrait approximationsfor nonlinear hybrid systems. In: Proceedingsof Hybrid Systems’95. 1995, 377–388
|
|
Podelski A, Rybalchenko A. A complete method for thesynthesis of linear ranking functions. In: Proceedings of VMCAI’04. 2004, 239–251
|
|
Tiwari A. Terminationof linear programs. In: Proceedings ofCAV’04. 2004, 70–82
|
|
Yang L. Recentadvances on determining the number of real roots of parametric polynomials. J. Symbolic Computation, 1999, 28: 225–242
|
|
Yang L, Hou X, Xia B. A complete algorithm for automated discovering of a classof inequality-type theorems. Sci. in China(Ser. F), 2001, 44: 33–49
|
|
Yang L, Hou X, Zeng Z. A complete discrimination system for polynomials. Science in China (Ser. E), 1996, 39: 628–646
|
|
Xia B, Yang L. An algorithm for isolatingthe real solutions of semi-algebraic systems. J. Symbolic Computation, 2002, 34: 461–477
|
|
Xia B, Zhang T. Real solution isolation usinginterval arithmetic. Comput. Math. Appl., 2006, 52: 853–860
|
|
Yao Y. Terminationof nonlinear programs over intervals. Journalof Software (in press, in Chinese)
|
|
Xu M, Chen L, Li Z B. Reachability computation of a class of nonlinear systems. In: Proceedings of International Conference onComputer and Information Science’09. 2009, 706–710
|
|
Xu M, Chen L, Zeng Z, et al. Reachability analysis of rational eigenvaluelinear systems. To appear in InternationalJournal of Systems Science
|
|
Floyd R W. Assigning meanings to programs. In: Proceedingsof Symphosium on Applied Mathematics. 1967, 19–37
|
|
Hoare C A R. An axiomatic basis for computer programming. Comm. ACM, 1969, 12(10): 576–580
|
|
Naur P. Proofsof algorithms by general snapshops. BIT, 1966, 6: 310–316
|
|
German S, Wegbreit B. A synthesizer of inductiveassertions. IEEE Transactions on SoftwareEngineering, 1975, 1(1): 68–75
|
|
Karr M. Affinerelationships among variables of a program. Acta Informatica, 1976, 6:133–151
|
|
Katz S, Manna Z. Logical analysis of programms. Communications of the ACM, 1976, 19(4): 188–206
|
|
Wegbreit B. Thesynthesis of loop predicates. Communicationsof the ACM, 1974, 17(2): 102–112
|
|
Besson F, Jensen T, Talpin J P. Polyhedral analysis of synchronous languages. In: Proceedings of SAS’99. 1999, 51–69
|
|
Cousot P. Provingprogram invariance and termination by parametric abstraction, Langrangianrelaxation and semidefinite programming. In: Proceedings of VMCAI 2005. 2005, 1–24
|
|
Cousot P, Halbwachs N. Automatic discovery of linearrestraints among the variables of a program. In: Proceedings of ACM POPL’78. 1978, 84–97
|
|
Colón M, Sankaranarayanan S, Sipma H B. Linear invariant generation using non-linearconstraint solving. In: Proceedings ofCAV’03. 2003, 420–432
|
|
Mueller-Olm M, Seidl H. Polynomial constants aredecidable. In: Proceedings of 9th StaticAnalysis Symposium (SAS’02). 2002, 4–19
|
|
Mueller-Olm M, Seidl H. Precise interprocedural analysisthrough linear algebra. In: Proceedingsof ACM POPL’04. 2004, 330–341
|
|
Rodriguez-Carbonell E, Kapur D. Generating all polynomialinvariants in simple loops. Journal ofSymbolic Computation, 2007, 42: 443–476
|
|
Davenport J H, Heintz J. Real elimination is doublyexponential. J. of Symbolic Computation, 1988, 5: 29–37
|
|
Colón M, Sipma H B. Synthesis of linear rankingfunctions. In: Proceedings of TACAS’01. 2001, 67–81
|
|
Dams D, Gerth R, Grumberg O. A heuristic for the automatic generation of ranking functions. In: Proceedings of Workshop on Advances in Verification(WAVe’00). 2000, 1–8
|
|
Chen Y, Xia B, Yang L, et al. Discovering non-linear ranking functions bysolving semi-algebraic systems. In: Proceedingsof ICTAC’07. 2007, 34–49
|
|
Bradley A, Manna Z, Sipma H. Termination of polynomial programs. In: Proceedings of VMCAI’05. 2005
|
|
Braverman M. Terminationof integer linear programs. In: Proceedingsof CAV’06. 2006, 372–385
|
|
Xia B. DISCOVERER:a tool for solving semi-algebraic systems. ACM SIGSAM Bulletin, 2007, 41(3): 102–103
|
|
Chen Y, Xia B, Yang L, et al. Generating polynomial invariants with DISCOVERERand QEPCAD. In: Proceedings of Formal Methodsand Hybrid Real-Time Systems’07 (the Festschrift Symposiumfor Dines Bjorner and Zhou Chaochen). 2007, 67–82
|
|
Xia B, Yang L, Zhan N. Program verification by reduction to semi-algebraic systemssolving. In: Proceedings of ISoLA’08. 2008, 277–291
|
|
Li Y. Automaticdiscovery of non-linear ranking function of loop programs. ICCSIT, 2009, 1: 402–406
|
|
Bradley A, Manna Z, Sipma H. Termination analysis of integer linear loops. LNCS 3653, 2005, 488–502
|
|
Yang L. Recentadvances in automated theorem proving on inequalities. J. of Computer Science and Technology, 1999, 14(5): 434–446
|
|
Xia B, Yang L, Zhan N, et al. Symbolic decision procedure for terminationof linear programs. (DOI:10.1007/s00165-009-0144-5), Formal Aspects of Computing (in press)
|
|
Bi Z, Shan M. Termination analysis of linearprograms with conditionals. In: Proceedingsof International Conference on Advanced Computer Theory and Engineering’08. 2008, 450–456
|
|
Blondel V D, Bournez O, Koiran P, et al. Deciding stability and mortality of piecewiseaffine dynamical systems. Theoretical ComputerScience, 2001, 255(1–2): 687–696
|
|
Xia B, Zhang Z. Termination of linear programswith nonlinear constraints. arXiv:0904.3588v1, 2009
|
|
Wu B, Shen L, Bi Z. Termination of loop programs with polynomial guards.In: Proceedings of the 2010 International Conference on ComputationalScience and Its Applications, LNCS (in press)
|
|
Wu B, Shen L, Bi Z, et al. Termination of a class of the programs withpolynomial guards. In: Proceedings of InternationalConference on Information Management and Engineering. 2009, 274–277
|
|
Bi Z, Shan M, Wu B. Termination analysis of P-solvable loops with assignmentsonly. In: Proceedings of 2008 InternationalSymposium on Information Science and Engineering. 2008, 125–129
|
|
Kovács L. Automatedinvariant generation by algebraic techniques for imperative programverification in theorema. Dissertation for the Doctoral Degree. Hohannes Kepler University of Linz, 2007
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
