Madiel de Souza Conserva Filho / ZB2SMT

Blame view

ZB2SMT/zb2smtsite/index.html 5.13 KB
edit raw normal view history
22e44bf4e   Madiel de Souza Conserva Filho   first 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
 
  <?xml version="1.0"?>
  <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
  <html xmlns="http://www.w3.org/1999/xhtml" xml:lang="cs" lang="cs"><!-- InstanceBegin template="/Templates/template.dwt" codeOutsideHTMLIsLocked="false" -->
  <head>
      <meta http-equiv="content-type" content="text/html; charset=utf-8" />
      <meta http-equiv="content-language" content="cs" />
      <meta name="robots" content="all,follow" />
  
      <meta name="author" content="All: ... [Nazev webu - www.url.cz]; e-mail: info@url.cz" />
      <meta name="copyright" content="Design/Code: Vit Dlouhy [Nuvio - www.nuvio.cz]; e-mail: vit.dlouhy@nuvio.cz" />
      <!-- InstanceBeginEditable name="doctitle" -->
      <title>ZB2SMT</title>
      <!-- InstanceEndEditable -->
      <meta name="description" content="..." />
      <meta name="keywords" content="..." />
      
      <link rel="index" href="../." title="Home" />
      <link rel="stylesheet" media="screen,projection" type="text/css" href="css/main.css" />
      <link rel="stylesheet" media="print" type="text/css" href="css/print.css" />
      <link rel="stylesheet" media="aural" type="text/css" href="css/aural.css" />
      <!-- InstanceBeginEditable name="head" --><!-- InstanceEndEditable -->
  </head>
  
  <body id="www-url-cz">
  
  <!-- Main -->
  <div id="main" class="box">
  
      <!-- Header -->
      <div id="header">
  
          <!-- Logotyp -->
          <h1 id="logo" title="Integrating Z and B tools with SMT-solvers">ZB2SMT</h1>
          <hr class="noscreen" />          
  
      </div> <!-- /header -->
  
       <!-- Main menu (tabs) -->
       <div id="tabs" class="noprint">
              <h3 class="noscreen">Navigation</h3>
              <ul class="box">
                  <li  id="active"><a href="home.html">Home<span class="tab-l"></span><span class="tab-r"></span></a></li>
                  <li><a href="download.html">Download<span class="tab-l"></span><span class="tab-r"></span></a></li>
                  <li><a href="doc.html">Documentation<span class="tab-l"></span><span class="tab-r"></span></a></li>
                  <li><a href="people.html">People<span class="tab-l"></span><span class="tab-r"></span></a></li>
                  <li><a href="support.html">Support<span class="tab-l"></span><span class="tab-r"></span></a></li>
                  <li><a href="links.html">Related Links<span class="tab-l"></span><span class="tab-r"></span></a></li>
              </ul>
  
          <hr class="noscreen" />
       </div> <!-- /tabs -->
  
      <!-- Page (2 columns) -->
      <div id="page" class="box">
      <div id="page-in" class="box">
  
   
  
          <!-- Content -->
          <!-- InstanceBeginEditable name="content" -->
          <div id="content">
            <!-- Article -->
            <div class="article">
              <h2><span>What is ZB2SMT?</span></h2>
              <p>ZB2SMT is a Java package integrated with <a href="http://www.smt-lib.org/">SMT</a>(Satisfiability Modulo Theories) solvers. The motivation for our work is to provide an automatic verification engine to discharge proof obligations from Z, B or extensions of their, tools. The package takes predicates from both the Z and the B notations and yields a boolean value for them.</p>
  			<p> ZB2SMT uses an extension of BOL to represent B predicates. On the other hand, the package uses a framework provided by the <a href="http://czt.sourceforge.net/">CZT</a>(Community Z Tool), an ongoing effort that implements tools for standard Z, to represent Z predicates. It also provides methods for get a SMT-file that represents a Z/B predicate. This file can be used as input in most SMT solvers, such as: <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/index.html">Z3</a>, <a href="http://www.cs.nyu.edu/acsys/cvc3/">CVC3</a> and <a href="http://www.verit-solver.org/">veriT</a>.</p>
            </div>
            <!-- /article -->
            <hr class="noscreen" />
            <hr class="noscreen" />
          </div>
          <!-- /content -->
          <!-- InstanceEndEditable -->
          <!-- Right column -->
          <div id="col" class="noprint">
              <div id="col-in">
          <!-- Links -->
                  <h3><span>Links</span></h3>
  
  
  				<p> <a href="http://sites.google.com/site/forallufrn/"> <img src="figures/ufrn.jpg" width="100" height="37"/> </a></p>
  				
  				<p> <a href="http://www.dimap.ufrn.br/" > <img src="figures/logo_dimap.gif" width="100" height="37" /> </a> </p>
  				
  				<p> <a href="http://www.ccet.ufrn.br/prh22/frame.htm"> <img src="figures/simb_PRH2.gif" width="100" height="37" /> </a> </p>
  				
  
                  <hr class="noscreen" />
              
              </div> <!-- /col-in -->
          </div> <!-- /col -->
  
      </div> <!-- /page-in -->
      </div> <!-- /page -->
  
      <!-- Footer -->
      <div id="footer">
          
          <hr class="noscreen" />
          
          <p id="createdby">created by <a href="http://www.nuvio.cz">Nuvio | Webdesign</a> <!-- DON´T REMOVE, PLEASE! --></p>
          <p id="copyright">&copy; 2010 <a href="mailto:alessandrogurgel@gmail.com">Alessandro Gurgel</a></p>
      </div> <!-- /footer -->
  
  </div> <!-- /main -->
  
  </body>
  <!-- InstanceEnd --></html>