E-FMP's Extensible Symbolic Execution Tool

Session details
Session Type: 
Experience level: 
Intermediate

Eclipse Formal Modeling Project -E-FMP for short- provides an extensible tool called SymbEx for the development of model-based formal analyses using symbolic execution. This is the first tool to be contributed to the E-FMP project. SymbEx comes with an expressive entry language that captures a wide range of classical models semantics: e.g., UML/SysML, SDL, (Timed) Symbolic Transition Systems and abstractions of Hybrid Automata... SymbEx provides developers with extension mechanisms allowing customizing the basic symbolic treatments to implement specific Formal Analysis Modules -FAM for short- (e.g., Model-based Testing -MBT for short- algorithms, exploration strategies and heuristics...). SymbEx is connected with SMT solvers, e.g., CVC4, Z3 and YICES which can be easily used to implement new FAMs. In fact, SymbEx provides "hooks" into the basic well-known symbolic execution algorithm which allow FAMs -by implementing specific pre-process or post-process or pre-filter or post-filter methods to customize symbolic treatments at different steps of the execution. We present these extensions facilities offered by the SymbEx tool. We also discuss how to use those facilities to develop some FAMs which implement reachability-based formal analyses up to coverage criteria.

Schedule info
Session Time Slot(s): 
Wednesday, June 13, 2018 - 15:45 to 16:20

Our Sponsors

For information about becoming a sponsor, please visit the EclipseCon France2018 sponsor prospectus page.

Premium

Basic

Regional Supporter

Conference App Provider

Media

JUG Partners

EclipseCon Support Other Events

Our Other Events

Eclipse events are hosted all over the world!

  • EclipseCon Europe 2018