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
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
Accelerated verification of parametric protocols with decision trees
Date de publication/diffusion :
2020
Nom de la manifestation :
38th International Conference on Computer Design
Date de la manifestation :
2020
Manifestation à portée :
International
Titre de l'ouvrage principal :
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.
