## Dancing with Pixies?...

At TEDx Tottenham, London Mark Bishop (the former chair of the Society) demonstrates that if the ongoing EU flagship science project - the 1.6 billion dollar "Human Brain Project” - ultimately succeeds in understanding all as...

Read More...

## Computerised Minds. ...

A video sponsored by the society discusses Searle's Chinese Room Argument (CRA) and the heated debates surrounding it. In this video, which is accessible to the general public and those with interest in AI, Olly's Philosophy Tube ...

Read More...

## Erden in AI roundtab...

On Friday 4th September, philosopher and AISB member Dr Yasemin J Erden, participated in an AI roundtable at Second Home, hosted by Index Ventures and SwiftKey. Joining her on the panel were colleagues from academia and indu...

Read More...

## AISB Convention 2016

The AISB Convention is an annual conference covering the range of AI and Cognitive Science, organised by the Society for the Study of Artificial Intelligence and Simulation of Behaviour. The 2016 Convention will be held at the Uni...

Read More...

## Bishop and AI news

Stephen Hawking thinks computers may surpass human intelligence and take over the world. This view is based on the ideology that all aspects of human mentality will eventually be realised by a program running on a suitable compu...

Read More...

## Connection Science

All individual members of The Society for the Study of Artificial Intelligence and Simulation of Behaviour have a personal subscription to the Taylor Francis journal Connection Science as part of their membership. How to Acce...

Read More...

## Al-Rifaie on BBC

AISB Committee member and Research Fellow at Goldsmiths, University of London, Dr Mohammad Majid al-Rifaie was interviewed by the BBC (in Farsi) along with his colleague Mohammad Ali Javaheri Javid on the 6 November 2014. He was a...

Read More...

## AISB YouTube Channel

The AISB has launched a YouTube channel: http://www.youtube.com/user/AISBTube (http://www.youtube.com/user/AISBTube). The channel currently holds a number of videos from the AISB 2010 Convention. Videos include the AISB round t...

Read More...

## Notice

# AISB event Bulletin Item

## Announcement: Satisfiability Modulo Theories Competition SMT-COMP 2007

CAV'07 Satellite Event 3rd International Satisfiability Modulo Theories Competition (SMT-COMP'07) Berlin, Germany July 2007 CALL FOR BENCHMARKS CALL FOR ENTRANTS =========================================================================== Decision procedures for checking satisfiability of logical formulas are crucial for many verification applications. Of particular recent interest are solvers for Satisfiability Modulo Theories (SMT). SMT-COMP aims to spur innovation in SMT research by providing a yearly friendly competition for SMT solvers. SMT-COMP came out of discussions surrounding the SMT-LIB initiative, an initiative of the SMT community to build a library of SMT benchmarks in a proposed standard format. SMT-COMP helps serve this goal by contributing collected benchmark formulas used for the competition to the library, and by providing an incentive for implementors of SMT solvers to support the SMT-LIB format. As part of SMT-COMP 2006, a special evening session was held at CAV 2006 in which the competitors had a chance to present their tools and discuss them with other competitors. This year, a similar session will be held as part of the SMT Workshop (July 1-2, affiliated with CAV). More information about the SMT Workshop can be found on the web page: http://www.lsi.upc.edu/~oliveras/smt07/ The highlights of SMT-COMP 2007 are covered below. For the latest information, please see the SMT-COMP web page at: http://www.smtcomp.org/ --------------- Benchmarks --------------- The potential benchmark divisions for this year include all of the divisions represented last year as well as new ones. For detailed descriptions of the divisions, refer to the SMT-LIB web page at http://www.smtlib.org/ * QF_UF (Uninterpreted Functions): This division consists of quantifier-free formulas whose satisfiability is to be decided modulo the empty theory. Each benchmark may introduce its own uninterpreted function and predicate symbols. * QF_IDL (Integer Difference Logic): This division consists of quantifier-free formulas to be tested for satisfiability modulo a background theory of integer arithmetic. The syntax of atomic formulas is restricted to difference logic, i.e. x - y op c, where op is either equality or inequality and c is an integer constant. * QF_RDL (Real Difference Logic): This division is like QF_IDL, except that the background theory is real arithmetic. * QF_UFIDL (Integer Difference Logic with Uninterpreted Functions): This division contains benchmarks in a logic which is similar to QF_IDL, except that it also allows uninterpreted functions and predicates. * QF_LIA (Linear Integer Arithmetic): This division consists of quantifier-free formulas to be tested for satisfiability modulo a background theory of integer arithmetic. The syntax of atomic formulas is restricted to contain only linear terms. * QF_LRA (Linear Real Arithmetic): This division is like QF_LIA, except that the background theory is real arithmetic. * QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions): This division contains benchmarks in a logic which is similar to QF_LIA, except that it also allows uninterpreted functions and predicates. * QF_UFLRA (Linear Real Arithmetic with Uninterpreted Functions): This division contains benchmarks in a logic which is similar to QF_LRA, except that it also allows uninterpreted functions and predicates. * QF_A (Arrays): Quantifier-free formulas over the theory of arrays (with extensionality). * QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions and Arrays): This division consists of quantifier-free formulas to be tested for satisfiability modulo a background theory combining linear integer arithmetic, uninterpreted function and predicate symbols, and extensional arrays. * QF_UFBV (Bit-vectors and Uninterpreted Functions) Unquantified formulas over bit vectors of fixed size, with unintepreted function and predicate symbols. * QF_AUFBV (Bit-vectors with arrays and Uninterpreted Functions) Unquantified formulas over bit vectors of fixed size, with arrays and unintepreted function and predicate symbols. * AUFLIA: (Linear Integer Arithmetic with Uninterpreted Functions and Arrays) This division consists of formulas with quantifiers to be tested for satisfiability modulo a background theory combining linear integer arithmetic, uninterpreted function and predicate symbols, and extensional arrays. * AUFLIRA: (Arrays, Uninterpreted Functions, and Linear Arithmetic) This division consists of formulas with quantifiers, arrays of reals indexed by integers (Array1), arrays of Array1 indexed by integers (Array2), and linear arithmetic over the integers and reals. This division is included to accommodate a large number of quantified verification benchmarks that have become available. As with last year, we reserve the right to remove benchmark divisions if we do not receive enough quality benchmarks or enough solvers in a particular division. If you have access to benchmarks in any of these divisions, even if they are not in the SMT-LIB format, please contact one of the organizers (see below). --------------- Solvers --------------- Please refer to http://www.smtcomp.org/ for complete details on entering the competition. --------------- Travel Grants --------------- Microsoft Research has generously donated funds to help pay for travel for participants, especially students, who might otherwise be unable to attend. Because funds are limited, we will use a bidding process to assign grants. The process works like this: 1. Those interested should send an email by June 1 to Clark Barrett indicating: * Your name and affiliation. * Whether you are a student. * The name of the solver you are submitting and your role in the development of the solver. * The amount of assistance you would need to be able to attend. 2. On or before June 11, we will notify those whose bids have been accepted (acceptance will be based primarily on the amount requested, with lower bids having precedence, but we will also take into account the role of the applicant in the development of the solver and whether or not the applicant is a student). 3. Following the conclusion of the competition, reimbursement checks will be issued to those whose bids were accepted and who attended. --------------- Important Dates --------------- * May 1: First version of the benchmark library posted for comment. * June 1: Revised version of the benchmark library posted. Travel grant applications due. * June 7: Travel grant notifications sent. * June 15: System submission opened. * June 25: Final system descriptions due, with magic numbers for pseudo-random selection of benchmarks. * July 1-2: SMT Workshop. * July 3-7: Anticipated dates for competition. ----------------- Organizers ----------------- Clark Barrett (New York University, barrett@cs.nyu.edu) Albert Oliveras (LSI Department, Technical University of Catalonia, oliveras@lsi.upc.edu) Aaron Stump (Washington University in St. Louis, stump@cse.wustl.edu) ---------------- More Information ---------------- For details on the competition, see http://www.smtcomp.org/ For more information on the SMT-LIB format, see http://www.smtlib.org/ For more information about the SMT Workshop, see http://www.lsi.upc.edu/~oliveras/smt07/ SMT-COMP is partially sponsored by the U.S. National Science Foundation, under grant CNS-0551697. |