Synthesizing Software Verifiers from Proof Rules S Grebenshchikov, NP Lopes, C Popeea, A Rybalchenko Proc. of the 33rd ACM SIGPLAN Conference on Programming Language Design and …, 2012 | 358 | 2012 |
Solving existentially quantified horn clauses TA Beyene, C Popeea, A Rybalchenko Computer Aided Verification: 25th International Conference, CAV 2013, Saint …, 2013 | 131 | 2013 |
Predicate abstraction and refinement for verifying multi-threaded programs A Gupta, C Popeea, A Rybalchenko Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2011 | 123 | 2011 |
A constraint-based approach to solving games on infinite graphs T Beyene, S Chaudhuri, C Popeea, A Rybalchenko Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014 | 116 | 2014 |
Inferring disjunctive postconditions C Popeea, WN Chin Annual Asian Computing Science Conference, 331-345, 2006 | 93 | 2006 |
HSF (C): A Software Verifier based on Horn Clauses S Grebenshchikov, A Gupta, NP Lopes, C Popeea, A Rybalchenko | 91* | 2012 |
Threader: A constraint-based verifier for multi-threaded programs A Gupta, C Popeea, A Rybalchenko Computer Aided Verification: 23rd International Conference, CAV 2011 …, 2011 | 80 | 2011 |
Analysing memory resource bounds for low-level programs WN Chin, HH Nguyen, C Popeea, S Qin Proceedings of the 7th international symposium on Memory management, 151-160, 2008 | 80 | 2008 |
Solving Recursion-Free Horn Clauses over LI+ UIF A Gupta, C Popeea, A Rybalchenko | 49 | 2011 |
Verifying safety policies with size properties and alias controls WN Chin, SC Khoo, S Qin, C Popeea, HH Nguyen Proceedings of the 27th international conference on Software engineering …, 2005 | 48 | 2005 |
Compositional Termination Proofs for Multi-Threaded Programs C Popeea, A Rybalchenko | 47 | 2012 |
A practical and precise inference and specializer for array bound checks elimination C Popeea, DN Xu, WN Chin Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and …, 2008 | 25* | 2008 |
Dual analysis for proving safety and finding bugs C Popeea, WN Chin Proceedings of the 2010 ACM Symposium on Applied Computing, 2137-2143, 2010 | 23 | 2010 |
A flow-based approach for variant parametric types WN Chin, F Craciun, SC Khoo, C Popeea ACM SIGPLAN Notices 41 (10), 273-290, 2006 | 20 | 2006 |
Reduction for compositional verification of multi-threaded programs C Popeea, A Rybalchenko, A Wilhelm 2014 Formal Methods in Computer-Aided Design (FMCAD), 187-194, 2014 | 15 | 2014 |
Threader: A Verifier for Multi-threaded Programs: (Competition Contribution) C Popeea, A Rybalchenko Tools and Algorithms for the Construction and Analysis of Systems: 19th …, 2013 | 15 | 2013 |
A type system for resource protocol verification and its correctness proof C Popeea, WN Chin Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and …, 2004 | 14 | 2004 |
Efficient CTL verification via horn constraints solving TA Beyene, C Popeea, A Rybalchenko arXiv preprint arXiv:1607.04456, 2016 | 11 | 2016 |
Towards a quantitative estimation of abstract interpretations F Logozzo, C Popeea, V Laviron Workshop on Quantitative Analysis of Software, 2009 | 10 | 2009 |
Recursive games for compositional program synthesis TA Beyene, S Chaudhuri, C Popeea, A Rybalchenko Verified Software: Theories, Tools, and Experiments: 7th International …, 2016 | 8 | 2016 |