SAT over an abstract domain
This is joint work with Vijay D’SIlva, Leopold Haller, and Michael Tautschnig. We present a generalisation of the DPLL(T) framework to abstract domains. As an instance, we present a sound and complete analysis for determining the range of floating-point variables in embedded control software. Existing approaches to bounds analysis either use convex abstract domains and are efficient but imprecise, or use floating-point decision procedures, and are precise but do not scale. We present a new analysis that elevates the architecture of a modern SAT solver to operate over floating-point intervals. In experiments, our analyser is consistently more precise than a state-of-the-art static analyser and significantly outperforms floating-point decision procedures.
Expressive power of logics with invariant uses of arithmetic predicates
In this talk I consider first-order formulas (FO, for short) where, apart from the symbols in the given vocabulary, also predicates for linear order and arithmetic may be used. For example, order-invariant formulas are formulas for which the following is true: If a structure satisfies the formula with one particular linear order of the structure's universe, then it satisfies the formula with any linear order of the structure's universe. Arithmetic-invariant formulas are defined analogously, where apart from the linear order other arithmetic predicates may be used in an invariant way. When restricting attention to finite structures, it is known that order-invariant FO is strictly more expressive than plain FO, and arithmetic-invariant FO can express exactly the properties that belong to the circuit complexity class AC0. On the other hand, by Trakthenbrot's theorem we know that order-invariance (on the class of finite structures) is undecidable. In this talk I want to give an overview of the state-of-the art concerning the expressive power of order-invariant FO and arithmetic-invariant FO.
PhD student Bursaries
The British Colloquium for Theoretical Computer Science is offering support for PhD students to attend BCTCS 2012 as follows
- Support towards BCTCS registration: £85
- Support towards accommodation: £25 per night up to a maximum of 3 nights
This means that the nett cost of registration for PhD students in receipt of bursaries will be £40, and the nett cost of accommodation will be approximately £23 per night (depending on hotel availavility). We regret that the reduced fee does not include the conference dinner.
Conditions:
Only PhD students may apply. Students are expected, in the normal course of events, to seek full funding from their university departments. All applicants must provide a signed letter from their PhD supervisors confirming their status as currently registered PhD students, and confirming also that their university department is unable to cover either the accommodation costs or the registration fee. If the applicant's department can cover the registration fee, but not the accommodation costs, then the applicant should request help with accommodation only. Help with accommodation costs will be given only if accommodation is booked through the official conference booking site using the cheapest available option (currently: IBIS Hotel). The number of bursaries is limited to 30, and will be distributed on a first-come-first served basis. Students applying for bursaries are encouraged to contribute talks, and are welcome to include a short abstract of their talks (approximately half a page) as a .pdf attachment, with their application.
How to apply
Applications for bursaries should be made in advance of registration, and sent by email to This e-mail address is being protected from spambots. You need JavaScript enabled to view it. , with the words "BCTCS student bursary" in the title. A signed letter of support from the applicant's supervisor should be attached as a .pdf file.
Payment
Notification of acceptance will be sent by email upon receipt of a valid application. Students in receipt of bursaries for registration will be given a password to select the reduced registration rate. Students in receipt of bursaries for accommodation costs will initially have to pay the hotel in full in the normal way, and will receive a refund afterwards, using a form which they will obtain at the conference.
