[1] Jung Y, Kong S, Wang B, et al. Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction[C]//Proc. of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation. Madrid, Spain: Springer, 2010. [2] Gopan D, Reps T W. Lookahead Widening[C]//Proc. of the 18th International Conference on Computer Aided Verification. Seattle, USA: Springer, 2006. [3] Bradley A R, Manna Z, Sipma H B. Linear Ranking with Reachability[C]//Proc. of the 17th International Conference on Computer Aided Verification. Edinburgh, UK: Springer, 2005. [4] Gulwani S, Srivastava S, Venkatesan R. Program Analysis as Constraint Solving[C]//Proc. of ACM SIGPLAN Conference on Programming Language Design and Implementation. Tucson, USA: ACM Press, 2008. [5] Kapur D. Automatically Generating Loop Invariants Using Quantifier Elimination[J]. Deduction and Applications, 2006, 64(1): 54-75. [6] Monniaux D. A Quantifier Elimination Algorithm for Linear Real Arithmetic[C]//Proc. of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Doha, Qatar: Springer, 2008. [7] Bradley A R, Manna Z. Property-directed Incremental Invari- ant Generation[J]. Formal Aspects of Computing, 2008, 20(4): 379-405. [8] Gupta A, Rybalchenko A. InvGen: An Efficient Invariant Generator[C]//Proc. of the 21th International Conference on Computer Aided Verification. Grenoble, France: Springer, 2009. [9] Hart T E, Ku K, Gurfinkel A, et al. Ptyasm: Software Model Checking with Proof Templates[C]//Proc. of the 23th IEEE/ ACM International Conference on Automated Software Engineering. L'Aquila, Italy: IEEE Press, 2008. [10] Podelski A, Rybalchenko A. A Complete Method for the Synthesis of Linear Ranking Functions[C]//Proc. of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation. Venice, Italy: Springer, 2004. [11] Lalire G, Argoud M, Jeannet B. Interproc[EB/OL]. (2008-10- 21). http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/ interproc/index.html. [12] Moy Y, Marché C. Modular Inference of Subprogram Contracts for Safety Checking[J]. Journal of Symbolic Computation, 2010, 45(11): 1184-1211. [13] 邢建英, 李梦君, 李舟军. CILinear: 一个线性不变式自动构造工具[J]. 计算机科学, 2010, 37(12): 91-95. [14] Jung Y, Kong S, David C, et al. Automatically Inferring Loop Invariants via Algorithmic Learning[C]//Proc. of MSCS’12. [S. 1.]: IEEE Press, 2012. [15] Ernst M D, Perkins J H, Guo P J, et al. The Daikon System for Dynamic Detection of Likely Invariants[J]. Science of Computer Programming, 2007, 69(1-3): 35-45. [16] Furia C A, Meyer B. Inferring Loop Invariants Using Post- conditions[M]. Berlin, Germany: Springer [s. n.], 2010. [17] Sharma R, Dillig I, Dillig T, et al. Simplifying Loop Invariant Generation Using Splitter Predicates[C]//Proc. of the 23th International Conference on Computer Aided Verification. Cliff Lodge, USA: Springer, 2011. [18] Kovács L, Voronkov A. Finding Loop Invariants for Programs over Arrays Using a Theorem Prover[C]//Proc. of the 12th International Conference on Fundamental Approaches to Software Engineering. York, UK: Springer, 2009. 编辑 索书志 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|