3 papers
cs.LO2015
Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems (extended version)
Alessandro Trindade, Hussama Ismail, Lucas Cordeiro
We present an alternative approach to solve the hardware (HW) and software (SW) partitioning problem, which uses Bounded Model Checking (BMC) based on Satisfiability Modulo Theorie…
cs.LO2015
Model Checking Embedded C Software using k-Induction and Invariants (extended version)
Herbert Rocha, Hussama Ismail, Lucas Cordeiro +1
We present a proof by induction algorithm, which combines k-induction with invariants to model check embedded C software with bounded and unbounded loops. The k-induction algorithm…
cs.LO2015
Model Checking C Programs with Loops via k-Induction and Invariants
Herbert Rocha, Hussama Ismail, Lucas Cordeiro +1
We present a novel proof by induction algorithm, which combines k-induction with invariants to model check C programs with bounded and unbounded loops. The k-induction algorithm co…