抄録
Offer Organization: Japan Society for the Promotion of Science, System Name: Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (B), Category: Grant-in-Aid for Young Scientists (B), Fund Type: -, Overall Grant Amount: - (direct: 3300000, indirect: 990000)
In this research, we developed an efficient method for computationally hard problems that intrinsically require us to enumerate all solutions of constraint satisfaction problems (CSPs). As a major achievement, we developed a computer-aided method to help us to locate faults in the designs of hardware and software. Model checking is a widely applied method for the verification and debugging of information systems. A counterexample is detected from an erroneous system as a proof of error by executing model checking, however, there is a big gap between computing counterexamples and locating faults. We thus proposed a method for providing information regarding error in a more understandable form than counterexamples by abstracting many counterexamples, which is expected to aid us in moving a trace of failure (i.e., a counterexample) to an understanding of the essence of the failure.
Beside the model checking application, we tackled security/privacy-related researches.