Software Model Checking in the Multicore Era

contact: ahmed rezine

ceniit project 12.04

Publications (in part) supported by Ceniit

The following page is lazily maintained. You might want to check out here, or dblp or google.

journals:

conferences:

  • Accepted TRAU: SMT solver for string constraints, at the International Conference on Formal Methods in Computer-Aided Design, FMCAD 18

  • Stability-aware integrated routing and scheduling for control applications in Ethernet networks, at Design, Automation and Test in Europe, DATE 2018

  • Safety Verification of Phaser Programs, at the International Conference on Formal Methods in Computer-Aided Design, FMCAD 17

  • Quantifying the Information Leak in Cache Attacks via Symbolic Execution, at the 15th ACM-IEEE International Conference on Formal Methods and Models for System Designn, MEMOCODE 17

  • Flatten and Conquer (A Framework for Efficient Analysis of String Constraints), at the 38th annual ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI 17

  • Accepted Lazy Constrained Monotonic Abstraction, at the 17th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI 2016.

  • Norn: An SMT Solver for String Constraints, at the 27th International Conference on Computer Aided Verification CAV 2015.

  • Verification of Cache Coherence Protocols wrt. Trace Filters, at the International Conference on Formal Methods in Computer-Aided Design, FMCAD 15

  • Abstracting and Counting Synchronizing Processes, at the 16th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI 2015.

  • String Constraints for Verification, at the 26th International Conference on Computer Aided Verification CAV 2014.

  • Ordered Counter-Abstraction: Refinable Subword Relations for Parameterized Verification, LATA 2014.

  • Verifying Safety and Liveness for the FlexTM Hybrid Transactional Memory at at Design, Automation and Test in Europe, DATE 2013.

  • ★Best paper award★ An Integrated Specification and Verification Technique for Highly Concurrent Data Structures at 19th International Conference Tools and Algorithms for the Construction and Analysis of SystemsTACAS 2013.

  • Memorax: Fence Inference under the TSO Memory Model at at 19th International Conference Tools and Algorithms for the Construction and Analysis of SystemsTACAS 2013.

  • Automatic Test Program Generation for Out-of-Order Superscalar Processors at the 21st IEEE Asian Test Symposium, ATS 2012.

  • Automatic Fence Insertion in Integer Programs via Predicate Abstraction at the 19th International Symposium on Static Analysis, SAS 2012.

  • Counter-Example Guided Fence Insertion under TSO at the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012.

  • miscellaneous: