148 articles – 163 Notices  [english version]

inria-00515167, version 1

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning

Yu-Fang Chen 1, Edmund M. Clarke a, 2, Azadeh Farzan b, Fei He () c, 3, 4, Ming-Hsien Tsai d, Yih-Kuen Tsay d, Bow-Yaw Wang () 3, Lei Zhu c

International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (2010)

Résumé : We compare two learning algorithms for generating contextual assumptions in automated assume-guarantee reasoning. The CDNF algorithm implicitly represents contextual assumptions by a conjunction of DNF formulae, while the OBDD learning algorithm uses ordered binary decision diagrams as its representation. Using these learning algorithms, the performance of assume-guarantee reasoning is compared with monolithic interpolation-based Model Checking in parametrized hardware test cases.

  • a –  Carnegie Mellon University
  • b –  Universityof Toronto
  • c –  Tsinghua University
  • d –  National Taiwan University
  • 1 :  Uppsala University
  • Uppsala University
  • 2 :  Computer Science Department in Carnegie Mellon University (CMU)
  • Carnegie Mellon University
  • 3 :  FORMES (LIAMA)
  • INRIA – Tsinghua University / Beijing – LIAMA
  • 4 :  Tsinghua University
  • Tsinghua University
  • Domaine : Informatique/Logique en informatique
  • Mots-clés : assume-guarantee reasoning – learning – model checking – formal verification
 
  • inria-00515167, version 1
  • http://hal.inria.fr/inria-00515167
  • oai:hal.inria.fr:inria-00515167
  • Contributeur : Bow-Yaw Wang <>
  • Soumis le : Lundi 6 Septembre 2010, 03:50:07
  • Dernière modification le : Lundi 6 Septembre 2010, 03:50:07