Links
Automated Reasoning
- Competitions:
SAT,
QBF,
CSP,
ASP,
first-order,
software model checking
-
A library of problems in classical logic. Also includes pointers to libraries of SAT, QBF, CSP, SMT, etc.:
Thousands of Problems for Theorem Provers (TPTP)
- Industrially successful applications:
Databases
(
Oracle,
MySQL,
SQLServer,
DB2,
Sybase
),
Formal methods (
Intel,
Microsoft
)
- Incomplete list of researchers applying AR:
Security (
John Mitchell,
Cedric Fournet,
Anupam Datta ,
Alessandro Armando,
Frank Pfenning
),
Robotics (
Hadas Kress-Gazit,
Toronto's Cognitive Robotics Group
),
Programming Languages (
Armando Solar-Lezama,
anyone using static typing
),
Distributed Systems (
Joseph Hellerstein,
Boon Thau Loo
),
Formal Verification ( virtually everyone )
Web Development
|
|
