A Metric Encoding for Bounded Model Checking (extended version)

Details A Metric Encoding for Bounded Model Checking (extended version) A Metric Encoding for Bounded Model Checking (extended version)

2009-07-17

arxiv.org/abs/0907.3085v2

Computer Science

Logic in Computer Science

Scientific paper

In Bounded Model Checking both the system model and the checked property are translated into a Boolean formula to be analyzed by a SAT-solver. We introduce a new encoding technique which is particularly optimized for managing quantitative future and past metric temporal operators, typically found in properties of hard real time systems. The encoding is simple and intuitive in principle, but it is made more complex by the presence, typical of the Bounded Model Checking technique, of backward and forward loops used to represent an ultimately periodic infinite domain by a finite structure. We report and comment on the new encoding technique and on an extensive set of experiments carried out to assess its feasibility and effectiveness.

Affiliated with

Also associated with

No associations

Rating

A Metric Encoding for Bounded Model Checking (extended version) does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A Metric Encoding for Bounded Model Checking (extended version), we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Metric Encoding for Bounded Model Checking (extended version) will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-110858