[PPL-devel] [GIT] ppl/w3ppl(master): Added YangWGI09. Non-ASCII characters removed.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at 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.",
 }
+
+ at 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."
+}