Model Checking in the Absence of Code, Model and Properties

• Main Authors: LO, David, KHOO, Siau-Cheng
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2007
• Subjects: preliminary study; model checking; formal property; model checking tool; execution trace; software correctness; available input; binary version; temporal property; commercial off-the-shelf; automatic way; enable execution trace; instrumentation tool; widespread industrial adoption; major approach; third party vendor; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/1279; https://ink.library.smu.edu.sg/context/sis_research/article/2278/viewcontent/ModelChecking_AbCode_2007.pdf
• Institution: Singapore Management University

Model checking is a major approach in ensuring software correctness. It verifies a model converted from code against some formal properties. However, difficulties and programmers ’ reluctance to formalize formal properties have been some hurdles to its widespread industrial adoption. Also, with the...