Madiel de Souza Conserva Filho / ZB2SMT

index.html 5.13 KB
edit raw blame history 
   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>