You are here: Home Team Mohammed Nassim Seghir

Mohammed Nassim Seghir

 

Research Interests

software model checking, software verification using SMT solvers, program analysis.

Publications

  • A Lightweight Approach for Loop Summarization. To appear in the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011.
  • An Assume Guarantee Approach for Checking Quantified Array Assertions. To appear In the 13th International Conference on Algebraic Methodology and Software Technology , AMAST 2010.
  • Abstraction Refinement for Quantified Array Assertions. In the 16th International Static Analysis Symposium, SAS 2009. With Andreas Podelski and Thomas Wies.
  • ACSAR: Software Model Checking with Transfinite Refinement. In the 14th International Workshop on Model Checking Software, SPIN 2007. With Andreas Podelski.
  • Integration of a Software Model Checker into Isabelle. In the 12th International Conference on Logic for programming, Artificial Intelligence and Reasoning, LPAR 2005. With Matthias Daum, Stefan Maus and Norbert Schirmer.

Talks

  • An Assume Guarantee Approach for Checking Quantified Array Assertions, AMAST 2010, Quebec.
  • Abstraction Refinement for Quantified Array Assertions. SAS 2009, Los Angeles.
  • ACSAR: Software Model Checking with Transfinite Refinement. SPIN 2007, Berlin.
  • Accelerating Abstraction Refinement by Summarizing Loops. Dagstuhl seminar on Software Verification: Infinite-State Model Checking and Static Program Analysis, February 06.

PhD thesis

  • Abstraction Refinement Techniques for Software Model Checking, December 2010.

Software

  • ACSAR - Automatic Checker for Safety properties based on Abstraction Refinement.
  • LotoStem - Tool for specification and verification of concurrent systems based on LOTOS.