Pang, Jun ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS) ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Wei, Xiaotao
External co-authors :
yes
Language :
English
Title :
Accelerated verification of parametric protocols with decision trees
Publication date :
2020
Event name :
38th International Conference on Computer Design
Event date :
2020
Audience :
International
Main work title :
Proceedings of the 38th International Conference on Computer Design (ICCD)
D. L. Dill, "The Mur' verification system," in Proc. 8th International Conference on Computer Aided Verification (CAV'96), ser. Lecture Notes in Computer Science, vol. 1102. Springer, 1996, pp. 390-393.
C. N. Ip and D. L. Dill, "Efficient verification of symmetric concurrent systems," in Proc. 11th International Conference on Computer Design (ICCD'93). IEEE, 1993, pp. 230-234.
S. C. C. Blom, J. R. Calame, B. Lisser, S. M. Orzan, J. Pang, J. C. van de Pol, M. Torabi Dashti, and A. J. Wijs, "Distributed analysis with µCRL: a compendium of case studies," in Proc. 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), ser. Lecture Notes in Computer Science, vol. 4424. Springer, 2007, pp. 683-689.
K. L. McMillan, Symbolic Model Checking. Kluwer, 1993.
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, "Symbolic model checking without BDDs," in Proc. 5th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), ser. Lecture Notes in Computer Science, vol. 1579. Springer, 1999, pp. 193-207.
C. Chou, P. K. Mannava, and S. Park, "A simple method for parameterized verification of cache coherence protocols," in Proc. 5th International Conference on Formal Methods in Computer-Aided Design, ser. Lecture Notes in Computer Science, vol. 3312. Springer, 2004, pp. 382-398.
Y. Li, K. Duan, D. N. Jansen, J. Pang, L. Zhang, Y. Lv, and S. Cai, "An automatic proving approach to parameterized verification," ACM Transactions on Computational Logic, vol. 19, no. 4, pp. 27:1-27:25, 2018.
Y. Li, K. Duan, Y. Lv, J. Pang, and S. Cai, "A novel approach to parameterized verification of cache coherence protocols," in Proc. 34th IEEE International Conference on Computer Design (ICCD'16). IEEE, 2016, pp. 560-567.
Y. Li, J. Cao, and J. Pang, "A learning-based framework for automatic parameterized verification," in Proc. 37th IEEE International Conference on Computer Design (ICCD'19). IEEE Computer Society, 2019, pp. 450-459.
J. Cao, Y. Li, and J. Pang, "L-CMP: An automatic learning-based parameterized verification tool," in Proc. 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE'18). ACM Press, 2018, pp. 892-895.
T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, ser. Lecture Notes in Computer Science. Springer, 2002, vol. 2283.
J. R. Quinlan, "Induction of decision trees," Machine Learning, vol. 1, no. 1, pp. 81-106, 1986.
-, C4.5: Programs for Machine Learning. Morgan Kaufmann, 1993.
L. Breiman, J. H. Friedman, R. A. Olshen, and C. J. Stone, Classification and Regression Trees. Chapman & Hall/CRC, 1984.
S. M. German, "Personal communications," 2000.
P. Garg, C. Löding, P. Madhusudan, and D. Neider, "Ice: A robust framework for learning invariants," in Proc. 26th International Conference on Computer Aided Verification (CAV'14), ser. Lecture Notes in Computer Science, vol. 8559. Springer, 2014, pp. 69-87.
P. Garg, D. Neider, P. Madhusudan, and D. Roth, "Learning invariants using decision trees and implication counterexamples," in Proc. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'16). ACM, 2016, pp. 499-512.
A. Cohen and K. S. Namjoshi, "Local proofs for global safety properties," Formal Methods in System Design, vol. 34, no. 2, pp. 104-125, 2009.
O. Grinchtein, M. Leucker, and N. Piterman, "Inferring network invariants automatically," in Proc. 3rd International Joint Conference on Automated Reasoning (IJCAR'06), ser. Lecture Notes in Computer Science, vol. 4130. Springer, 2006, pp. 483-497.
S. K. Lahiri and R. E. Bryant, "Constructing quantified invariants via predicate abstraction," in Proc. 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04), ser. Lecture Notes in Computer Science, vol. 2937. Springer, 2004, pp. 267-281.
K. L. McMillan, "Quantified invariant generation using an interpolating saturation prover," in Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), ser. Lecture Notes in Computer Science, vol. 4963. Springer, 2008, pp. 413-427.
S. Conchon, A. Goel, S. Krstic, A. Mebsout, and F. Zaïdi, "Cubicle: A parallel smt-based model checker for parameterized systems - tool paper," in Proc. 24th International Conference on Computer Aided Verification (CAV'12), ser. Lecture Notes in Computer Science, vol. 7358. Springer, 2012, pp. 718-724.
A. Pnueli, S. Ruah, and L. D. Zuck, "Automatic deductive verification with invisible invariants," in Proc. 7th International Conference Tools and Algorithms for the Construction and Analysis of Systems, (TACAS'01), ser. Lecture Notes in Computer Science, vol. 2031. Springer, 2001, pp. 82-97.
Y. Lv, H. Lin, and H. Pan, "Computing invariants for parameter abstraction," in Proc. 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE'07). IEEE CS, 2007, pp. 29-38.
S. Conchon, A. Goel, S. Krstic, A. Mebsout, and F. Zaïdi, "Invariants for finite instances and beyond," in Formal Methods in Computer-Aided Design (FMCAD'13). IEEE CS, 2013, pp. 61-68.
