Modeling, Optimization and Computation for Software Verification
作者： Mardavij Roozbehani , Eric Feron , Alexandre Megrestki
DOI: 10.1007/978-3-540-31954-2_39
关键词: Theoretical computer science 、 Source code 、 Computer science 、 Software design 、 Dynamic program analysis 、 Static program analysis 、 Semidefinite programming 、 Software construction 、 Software verification 、 Search-based software engineering
摘要: Modeling and analysis techniques are presented for real-time, safety-critical software. Software is the task of verifying whether computer code will execute safely, free run-time errors. The critical properties that prove safe execution include bounded-ness variables termination program in finite time. In this paper, dynamical system representations programs along with specific models pertinent to via an optimization-based search invariants developed. It shown automatic establish desired code, can be formulated as a convex optimization problem, such linear programming, semidefinite and/or sum squares programming.
springer.com
sci-hub.se 参考文章(24)
Anil Nerode, Panos J. Antsaklis, Wolf Kohn, Michael D. Lemmon, Shankar Sastry, Hybrid Systems V ,(1999)
Patrick Cousot, Semantic foundations of program analysis Prentice Hall. pp. 303- 342 ,(1981)
Moving horizon estimation for hybrid systems and fault detection american control conference. ,vol. 4, pp. 2471- 2475 ,(1999) , 10.1109/ACC.1999.786492
Gerardo Lafferriere, George J. Pappas, Shankar Sastry, Hybrid Systems with Finite Bisimulations Lecture Notes in Computer Science. pp. 186- 203 ,(1999) , 10.1007/3-540-49163-5_10
Michael A. Colón, Sriram Sankaranarayanan, Henny B. Sipma, Linear Invariant Generation Using Non-linear Constraint Solving computer aided verification. pp. 420- 432 ,(2003) , 10.1007/978-3-540-45069-6_39
M. Johansson, A. Rantzer, On the computation of piecewise quadratic Lyapunov functions conference on decision and control. ,vol. 4, pp. 3515- 3520 ,(1997) , 10.1109/CDC.1997.652393
Stephen Prajna, Ali Jadbabaie, Safety Verification of Hybrid Systems Using Barrier Certificates Hybrid Systems: Computation and Control. pp. 477- 492 ,(2004) , 10.1007/978-3-540-24743-2_32
John Tsitsiklis, Dimitris Bertsimas, Introduction to linear optimization ,(1997)
S. Hedlund, A. Rantzer, Optimal control of hybrid systems conference on decision and control. ,vol. 4, pp. 3972- 3977 ,(1999) , 10.1109/CDC.1999.827981
Patrick Cousot, Radhia Cousot, Systematic design of program analysis frameworks symposium on principles of programming languages. pp. 269- 282 ,(1979) , 10.1145/567752.567778