Module: ppl/w3ppl Branch: master Commit: e10b53a466b50d8d10821702a72b4faa06dbe657 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=e10b53a466b...

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Sat Apr 11 20:59:29 2009 +0200

Added YangWGI09. Non-ASCII characters removed.

---

htdocs/Documentation/ppl_citations.bib | 28 ++++++++++++++++++++++++++-- 1 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index aec1454..3ec2cb5 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -904,7 +904,7 @@ Year = 2008, Pages = "263--279", Abstract = "In 1995, HyTech broke new ground as a potentially - powerful tool for verifying hybrid systems –-- yet its + powerful tool for verifying hybrid systems --- yet its appicability remains limited to relatively simple systems. We address the main problems of HyTech with PHAVer, a new tool for the exact verification of safety @@ -2232,7 +2232,7 @@ additional optimisations, like conditional contextual constant folding, C++ method call devirtualization, an other contextual optimizations. - The compiler’s rich program manipulation + The compiler's rich program manipulation infrastructure facilitates the development of these advanced analysis capabilities. To facilitate the development high-level semantical analyses, a domain @@ -2471,3 +2471,27 @@ favorably to popular Boolean-level model checking algorithms based on BDDs and SAT.", } + +@Article{YangWGI09, + Author = "Z. Yang and C. Wang and A. Gupta and F. Ivan\v{c}i'{c}", + Title = "Model Checking Sequential Software Programs + Via Mixed Symbolic Analysis", + Journal = "ACM Transactions on Design Automation of Electronic Systems", + Volume = 14, + Number = 1, + Pages = "1--26", + Year = 2009, + ISSN = "1084-4309", + Publisher = "ACM Press", + Address = "New York, NY, USA", + Abstract = "We present an efficient symbolic search algorithm for + software model checking. Our algorithms perform + word-level reasoning by using a combination of decision + procedures in Boolean and integer and real domains, and + use novel symbolic search strategies optimized + specifically for sequential programs to improve + scalability. Experiments on real-world C programs show + that the new symbolic search algorithms can achieve + several orders-of-magnitude improvements over existing + methods based on bit-level (Boolean) reasoning." +}