Formal verification of synchronous data-flow program transformations toward certified compilers.
Van Chan NgoJean-Pierre TalpinThierry GautierPaul Le GuernicLoïc BesnardPublished in: Frontiers Comput. Sci. (2013)
Keyphrases
- data flow
- formal verification
- control flow
- program slicing
- model checking
- symbolic execution
- database machine
- bounded model checking
- automated verification
- model checker
- data transfer
- symbolic model checking
- digital signal processing
- object oriented software
- systolic array
- hardware and software
- programming language
- computer architecture
- temporal logic
- computer systems
- object oriented
- databases