Case Study: Miracor Medical Systems eliminates run‑time errors and reduces testing time with MathWorks Polyspace Code Prover

Miracor Eliminates Run-Time Errors and Reduces Testing Time for Class III Medical Device Software

Miracor Medical Systems, maker of the PiCSO Impulse System for improving microcirculation after stent implantation, faced the challenge of proving the safety and correctness of its Class III medical device software to meet CE and FDA requirements. Unit tests and code reviews left gaps in coverage across inputs, execution paths, and concurrency issues, so Miracor engaged MathWorks and adopted Polyspace Code Prover to add control‑flow and data‑flow semantic analysis and formal verification to their development process.

MathWorks provided training and Polyspace Code Prover analysis across roughly 25,000 lines of legacy and new C code, color‑coding operations to show proven‑safe, faulty, unreachable, or uncertain code. Using MathWorks’ tool, Miracor removed dead code, fixed divide‑by‑zero and buffer‑overflow defects, found concurrency risks, and instituted pre‑review static analysis—reducing the software footprint, focusing code reviews, speeding testing, and establishing verification evidence to support regulatory approval.

Miracor Medical Systems

Lars Schiemanck

Chief Technology Officer