Two columns ago, I focused on problems or puzzles to interest those unfamiliar with automated reasoning; but I also challenged researchers with problems of representation. One column ago, I offered a substantial challenge concerned with Tarskian geometry, an area of mathematics that offers surprises. So, you ask, What will take center stage in this column? Well, I have chosen to return to logic, specifically classical propositional logic, focusing on an area that might appear to be far simpler than it is.
Many years ago, I had the pleasure of working with Brandon Fitelson, Zach Ernst, and Ken Harris on various research topics. One of our favorite topics of investigation was new axiom systems for diverse areas of logic. Indeed, among other studies, we sought to derive one axiom system from another; the deriving of a known axiom system is one of the preferred ways of showing that a conjectured axiom system, sometimes a single axiom, has been found.
In this column, I focus on classical propositional logic. The inference rule to be used is, as expected and consistent with the role used in many areas of logic, condensed detachment, captured by the following clause in the presence of hyperresolution, where | denotes logical or and - denotes logical not.
% condensed detachment
-P(i(x,y)) | -P(x) | P(y).
But, you may well ask, Does this area of logic actually offer you interesting studies for automated reasoning? One reason that it merits experimentation rests with various axiom systems for this area of logic. At one end of the spectrum, Lukasiewicz and Meredith each offered a single axiom; in contrast, Frege much earlier offered a six-axiom system. I shall issue several challenges regarding these systems, some challenges easily met, and some that are not.
Frege offered the following six axioms, where the function i denotes implication and the function n denotes negation.
P(i(x,i(y,x))).
P(i(x,n(n(x)))). % relies on double negation
P(i(n(n(x)),x)). % relies on double negation
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).
P(i(i(x,y),i(n(y),n(x)))).
P(i(i(x,i(y,z)),i(y,i(x,z)))).
For the first challenge, I ask you to discover, among the six, that which is dependent, in other words provable from the other five. Once you have identified the dependent axiom, two sets of experiments might prove intriguing. In the first set, you pick one or more targets to prove and rely on the full set of six axioms, including the dependent one. In the second set, with the same target or targets, you seek proofs with a five-axiom set consisting of the independent set. Advantages exist with either approach; Bill McCune, author of OTTER, often preferred to conduct research with independent sets of axioms.
Next, I ask you to conjecture about the truth of the following statement: "Proofs of various axiom systems can be found when the automated reasoning program is constrained to discard any new item that rests on the use of double negation, even though two of Frege's six axioms employ double negation." Such a constraint provides an example of a restriction strategy. So, you are asked to take a stand: Use of this restriction strategy prevents the program from completing a proof of another axiom system, or this strategy does not block all such proofs. Of course, from earlier experiences or readings you may already know the answer. Whether you do or not, however, here are three questions to answer when comparing the use of blocking double negation versus allowing double negation:
In contrast to the challenges already offered, I now present challenges some of which I myself have not yet met. Specifically, I ask you to prove, with or without the cited restriction strategy, that the Frege six-axiom system implies the Meredith single axiom and also implies the Lukasiewicz single axiom for classical propositional logic, given each in negated form.
P(i(i(i(i(i(a1,a2),i(n(a3),n(a4))),a3),a5),i(i(a5,a1),i(a4,a1)))) |
$ANS(Meredith).
P(i(i(i(a1,a2),i(i(i(n(a3),n(a4)),a5),a3)),i(a6,i(i(a3,a1),i(a4,a1))))) |
$ANS(Lukasiewicz).
(You might prefer to rely on a Frege system in which the dependent axiom is removed, a topic I address in this column.) For those of you who enjoy history, Meredith found his 21-letter single axiom quite a few years after Lukasiewicz offered his 23-letter single axiom for the calculus.
Another area that I enjoyed pursuing with my colleagues involved circles of pure proofs. For example, if you have three axiom systems each consisting of a single member, a circle of pure proofs for this set of axiom systems would consist of a proof of B from A in which C is not allowed to participate, a proof of C from B in which A is not allowed to participate, and a proof of A from C in which B is not allowed to participate. The challenge I now offer is reminiscent of finding circles of pure proofs. You are asked to prove the following two Lukasiewicz 3-axiom systems, given in negated form, in such a manner that the proof of the first avoids using any member of the second, and the proof of the second avoids using any member of the first.
-P(i(i(p,q),i(i(q,r),i(p,r)))) | -P(i(i(n(p),p),p)) |
-P(i(p,i(n(p),q))) | $ANS(step_allLuka_1_2_3).
-P(i(i(i(p,q),r),i(q,r))) | -P(i(i(i(p,q),r),i(n(p),r))) |
-P(i(i(n(p),r),i(i(q,r),i(i(p,q),r)))) |
$ANS(step_allLuka_x_19_37_59).
This challenge is also reminiscent of the situation when one researcher asks another to find a proof that avoids some undesirable lemma.
I now turn the tables by focusing on the Meredith single axiom rather than the Frege system.
% Following is Meredith's single axiom for classical propositional logic..
P(i(i(i(i(i(x,y),i(n(z),n(u))),z),v),i(i(v,x),i(u,x)))).
I find interesting the fact that this axiom relies on five distinct variables in contrast to the Lukasiewicz single axiom that relies on six distinct variables. Meredith made two nice simplifications, that just cited and that regarding length. The challenge—impressive, I suspect—is to prove from the Meredith single axiom the Lukasiewicz single axiom. I have conducted a reasonably large set of experiments with this goal in mind, but I have not succeeded.
At this point, I imagine hearing a few of you asking for a monumental challenge, a challenge that perhaps cannot be met. For background, I note that Meredith supplied a proof for his single axiom, a proof that concludes by deducing a 3-axiom system by Lukasiewicz, the following frequently cited.
% Luka 1 2 3.
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(i(n(x),x),x)).
P(i(x,i(n(x),y))).
Yes, you are correct: These three axioms were offered earlier in a negated form. Meredith's proof has length 41 (applications of condensed detachment). After years of failed attempts, in 2000, with OTTER of course, I found a 38-step proof, also deducing the cited 3-axiom system of Lukasiewicz. Your monumental challenge is to find a proof that has length strictly less than 38 (applications of condensed detachment) and establishes the Meredith formula to be a single axiom for classical propositional logic. Clearly, you are permitted to choose a different axiom system as target. A word of warning is in order. Some may believe that finding a shorter proof of a member of a multiaxiom system promotes the finding of a shorter proof of the full target axiom system. In fact, unfortunately, and not so obvious, the aphorism "shorter subproofs do not necessarily a shorter total proof make" nicely summarizes the complexity of seeking proof abridgment.
If you find such a proof, I would greatly appreciate learning of it in detail. My 38-step proof, according to Fitelson, is most unusual in that, of the three targets to prove, the most difficult by far is actually proved second and used to prove the last.
And now, for the person who wonders whether experimenting with a simple problem or theorem can be fruitful, I borrow from history to answer the implied question. The set of support strategy was formulated to enable an Argonne program to prove a very, very simple theorem in group theory, a theorem that was at the time out of reach. Theorem: If in a group the square of every element x is the identity e, then the group is commutative. For a recent example, in a column published in 2010, I mentioned the subformula strategy, formulated to prove a Rezus formula of length 93, when the four axioms in use were each simple. Here is the Rezus single axiom for Ri with axioms B, C, I, and W:
P(i(i(i(x,i(i(i(y,y),i(i(z,z),i(i(u,u),i(i(v,v),
i(x,w))))),w)),i(i(i(i(i(v6,v7),i(i(v7,v8),i(v6,v8))),
i(i(i(i(i(v9,i(v9,v10)),i(v9,v10)),i(i(i(v11,v12),
i(i(v12,v13),i(v11,v13))),v14)),v14),v15)),v15),
(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),
i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)).
So, in keeping with my view that strategy is and will be the key to increasing the power of automated reasoning programs, I have offered here various challenges to spur the corresponding research.
An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people (listed in alphabetical order) are currently serving as trustees of CADE Inc.:
The current members of the board of trustees are (in alphabetical order):
The terms of Renate Schmidt and Christoph Weidenbach expire. Both have served for two terms, and therefore cannot be nominated for a third term. There are thus two positions of elected trustees to fill.
The following candidates were nominated and their statements are below
My scientific contributions comprise foundational research (e.g., semantics and proof theory of classical higher-order logic, generic reasoning framework for quantified non-classical logics), system development and system integration (e.g., Leo provers, O-Ants agent based reasoning framework, Omega proof assistant), reasoning infrastructures (e.g., TPTP THF, LeoPARD) and applications (e.g. in metaphysics, maths and AI).
I have been an active member of the CADE community for about two decades, and I have previously served as CADE trustee and as IJCAR steering committee member. I fully support the current scheme of interleaving CADE and IJCAR conferences. My service to the community furthermore includes PC memberships in e.g. numerous CADE, IJCAR, FroCoS, Tableaux conferences, reviewing for various journals and national funding bodies, and the organisation of scientific events. Just recently, I have organised the CADE-25 conference in Berlin which attracted more than 200 participants.
I have also helped to improve the visibility of our field in the wider community. For example, I have presented papers at ECAI and IJCAI conferences, where automated deduction is currently inadequately represented, and (jointly with colleagues) I have reached out to philosophy. Our contributions to computational metaphysics had a media repercussion on a global scale. Recently, I have also intensified my interaction with German national politics.
In my opinion our research area has a bright future ahead. An increased interest will particularly be triggered by applications and system deployment in novel domains. It is therefore important, that CADE conferences realise an adequate balance between theory contributions (our traditional focus), system descriptions, experiments and inspiring application papers.
My research focuses on theoretical, implementation and application aspects of automated reasoning. I have been working on instantiation-based methods, EPR-based verification, linear arithmetic, theory reasoning, ordering constraints, orientability and AC-orderings. I developed iProver, an instantiation-based theorem prover for first-order logic, which won the EPR and the first-order satisfiability divisions (FNT) at a number of recent CASC competitions. I gave invited talks at CADE-22, FroCos'13 and a number of workshops. I was a conference co-chair and co-organiser of IJCAR 2012, held at the University of Manchester. As such, I played an active role in attracting and supporting a large number of workshops (12), system competitions (4) and Woody Bledsoe Student Travel Awards (27).
CADE excels in combining diverse research communities and fosters rapidly growing and exciting areas. I believe this tradition is vital for the success of CADE. I strongly support the participation of CADE within IJCAR and FLoC which helps to achieve the goal of bringing together the wider research community. Likewise, I strongly support the organisation of workshops, tutorials and competitions co-located with CADE. I believe it is important to support not only well-established workshops but also smaller workshops/competitions promoting novel topics in the area. Attracting and supporting students and young researchers is vital for the future development of automated reasoning and CADE. For this it is important to have low student conference fees, secure funding for student travel awards and to involve students in on-site conference organisation. We had a rewarding experience at IJCAR 2012 with a large number of students supported by the Woody Bledsoe Awards.
CADE maintains a good balance between theoretical work, implementation and applications. I believe CADE can further strengthen interactions between the research community and real-world applications. I thoroughly support the development of new systems and competitions such as CASC/SMT-COMP/SAT Competition/Termination/OWL Reasoner Evaluation, which demonstrate the possibilities of state-of-the-art reasoning systems to a wide range of users and conversely, propagate problems from real-world applications to the research community. CADE should keep promoting best research and therefore I support the best paper awards and the recently introduced Skolem Award for influential papers in the field.
As a CADE trustee, I will be devoted in supporting and promoting high quality theoretical research, development of reasoning systems and interaction between theory and applications. I will do my best in attracting and supporting young researchers in the area.
After writing a few words about my involvement in CADE, I address a few issues that in my view need to be addressed by the Trustees and the community at large.
I have been attending CADE since 1994. I presented several papers at CADE and IJCAR and served on many program committees. Most recently, together with Amy Felty, I served as PC chair of the highly successful 25th edition in Berlin.
After spending more than ten years in Japan, since 2003 I lead a research group on computational logic in Innsbruck, in which automated deduction plays an important role. System descriptions and competitions are an essential part of CADE. Several software tools (on certification, confluence, theorem proving, to name a few) are developed in Innsbruck and we initiate/organize/host competitions (CoCo, TermCOMP) and workshops (IWC, WST) to advance the development of tools.
The following items mention some of the topics which I feel are important for the future of CADE. If elected as CADE trustee
My main research areas are automated and interactive theorem proving, program verification, and SMT solving. I have been member of the CADE/IJCAR community since I attended my first conference related to deduction, IJCAR 2004 in Cork. Since then, I have participated at most of the CADE/IJCAR conferences, published papers at several of them, entered the CASC competition every year since 2012, organised two workshops that were affiliated with IJCAR (LfSA in 2010, and SMT in 2014), and always enjoyed the friendly and open atmosphere at the conferences. Since 2014, I am also elected member of the steering committee of the SMT workshop, and I have served on the PC of various related conferences and workshops.
As a conference and community, CADE/IJCAR has developed well over the last years and managed to attract a stable number of submissions and attendees; but I believe that there are several challenges that the community has to keep in mind to stay relevant. One of those is to continue providing a forum for all forms of deduction; there is an ongoing diversification of theorem proving technology, which can quickly lead to new paradigms/techniques/communities that might not necessarily consider CADE/IJCAR as first affiliation. One example of the past years was the development of SMT, now increasingly being unified with first-order theorem proving (but still with publications more often at verification conferences than at CADE/IJCAR). A second example is the growing number of automated theorem provers for separation logic, and similar "new" logics inspired by applications. CADE/IJCAR has to reach out to such newly emerging fields to avoid getting sidelined, and to remain an attractive forum for a variety of deduction techniques.
A related challenge is to keep the conferences well connected with applications of computer-aided deduction, and to aim at broadening the scope of reasoning and deduction by inviting or welcoming contributions from new domains. CADE/IJCAR have always been venues for both theoretical and practical papers, but concrete applications motivating the research can be as important. This obviously includes verification, formalised mathematics, etc., areas where reasoning has been successful in the past; but also new domains that might result from the resurgence of AI in the past years (in academia and industry), among others. It is the responsibility of CADE/IJCAR to propagate the use of deduction and automated reasoning wherever it can be useful, and to motivate or initiate research that closes the gap between existing techniques and potential application domains.
We invite proposals for sites around the world to host the international Conference on Automated Deduction (CADE) to be held in summer 2017. CADE typically merges into IJCAR (the International Joint Conference in Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome. CADE's/IJCAR's recent location history is as follows:
The upcoming CADE/IJCAR event will be:
The deadline for proposals is 30 October 2015.
In addition, we encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal due date.
Proposals should address the following points that also represent criteria for evaluation:
Perspective organizers are encouraged to get in touch with the CADE secretary and president (at martingi (at) ifi.uio.no and mariapaola.bonacina (at) univr.it) for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is encouraged.
Registration for TABLEAUX/FroCoS 2015 in Wrocław is open.
Invited Speakers:
Tutorials:
Wrocław is a pleasant, moderately sized town in the center of Europe, approximately 350 km from Berlin, Prague and Warsaw. The old town is nice, and the conference is only 20 minutes walking away.
Early registration costs 1200 PLN (292 euro, 330 US dollar). See the web sites for details.
FMCAD will be co-located with the MEMOCODE and SAT conferences, and with the DIFTS and ACL2 workshops. The conference program will include, in addition to regular paper presentations, tutorials by Isil Dillig (UT Austin), Priyank Kalla (Utah), Andre Platzer (CMU), and Roderick Bloem (TU Graz); new editions of the Hardware Model Checking competition and the FMCAD Student Forum; and an industrial panel discussion on 'Formal Verification in the Industry—a 2020 Vision'. We also have confirmed keynote speakers including Sharad Malik (Princeton University) and ACM Turing Award winner E. Allen Emerson (University of Texas at Austin). See the conference web site for details.
In keeping with the tradition of LPAR, researchers and practitioners are invited to submit short presentation papers (the papers can be full length, the presentation slots will be short), reporting on interesting work in progress, system and tool descriptions, experimental results, etc. They need not be original, and extended or revised versions of the papers may be submitted concurrently with or after LPAR to another conference or a journal. Authors of accepted papers are required to ensure that at least one of them will be present at the conference.
The short presentation papers will be published electronically as a volume in the EPiC series. The paper submission deadline is 19 October 2015. However, To facilitate authors making travel arrangements, papers submitted before the deadline will be reviewed immediately, and a decision made in approximately one week. See the conference web site for details.
Contributions:
Proposals for mini symposia, workshops, tutorials [slide-deck posed on www.iaria.org], and panels: [slide-deck posed on www.iaria.org].
Tracks:
Submission deadline: 3 November 2015. See the web site for details.
The purpose of SCSS 2016 is to promote research on theoretical and practical aspects of symbolic computation in software science. The symposium provides a forum for active dialog between researchers from several fields of computer algebra, algebraic geometry, algorithmic combinatorics, computational logic, and software analysis and verification.
Abstracts are due by 13 November 2015. After the symposium, we will have a combined special issue of the Journal of Symbolic Computation on SCSS 2014 and 2016. See the symposium web page for details.
ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of five main annual conferences, accompanied by satellite workshops. ETAPS 2016 is the 19th event in the series.
Main conferences:
TACAS 2016 hosts the 5th Competition on Software Verification (SV-COMP). Around 20 satellite workshops will take place before and after the main conferences.
The submission deadline is 9 October 2015 for abstracts and 16 October 2015 for full papers. See the ETAPS web site for details.
ManyVal is a series of international workshops on the logical and algebraic aspects of many-valued reasoning. The aim of the workshops is to gather both established and young researchers sharing an interest for a specific topic. Accordingly, each edition has a sharp focus. The attendance will be limited in order to facilitate close and informal interaction. There are no parallel sessions and contributed talks are allocated ample time.
The theme of ManyVal 2015 is First-Order and Modal Many-Valued Logics.
Participants who wish to give a talk should submit an extended abstract (max. 2 pages written in plain LaTeX) before 25 September 2015. See the workshop web site for details.
You are invited to submit your contribution to the International Workshop on MILS, co-located with the HiPEAC Conference 2016. MILS is a high-assurance security architecture based on the concepts of separation and controlled information flow. The MILS architectural approach is all about decomposition of a system design into well-understood components and their interactions with the goal to achieve composable architecture and composable assurance for the designed system. The composability of architecture and assurance for secure systems is a grand challenge, which we undertake to meet using the MILS architectural approach.
The workshop topics are but not limited to
Submissions do not need to be full papers: this is a workshop and we are looking for interesting experience, work, and ideas (possibly preliminary and exploratory) that will stimulate discussion and thought around MILS concepts and challenges. Submissions should be in PDF format between 3-12 pages. We recommend the guidelines for ACM SIG Proceedings.
Position papers are due on 8 November 2015. See the workshop web page for details.
We are proud to announce that our book The Little Prover has recently become available. The book is a gentle introduction to formal logic, induction, and proofs about programs in the style of The Little Schemer, and its logic is based on the ACL2 theorem prover. You can find The Little Prover at Amazon (with a nice discount, but temporarily out of stock) and MIT Press, among others.
Our little book includes a little proof assistant called J-Bob in honor of J Moore and Bob Boyer. Thanks again, J and Bob. The full source code to our proof assistant, as well as a transcript of every proof in the book, is available online for ACL2 and Scheme.
Dracula, the Racket package for ACL2 integration, has also been updated to include the proof assistant J-Bob.
Happy reading.
Fifty to sixty mathematicians and computer scientists are invited to the IAS School of Mathematics each year to work to pursue research projects of their own, with each other or with the school faculty. A small number of memberships for a longer period of time (two years) are also available. Some mathematicians are supported by the Institute, while others receive financial aid from their home institutions, foundations or governments. While many members are at the postdoctoral level, the school hosts mathematicians at all stages of their careers. Special fellowships and joint programs with neighboring institutions are described below.
The deadline for School applications, as well as for the supporting letters of recommendation, is 1 December 2015. See the web site for details.
The chair Modeling and Analysis of Information Systems (MAIS) of Prof. Dr.-Ing. Heiko Mantel in the Department of Computer Science at TU Darmstadt, Germany, is offering two postdoc positions:
The detailed announcements contain information about the position descriptions, benefits, qualifications, and the application procedure.
The positions are available from 1 September 2015, but a later start is also possible. We will consider applications until the positions are filled.
Questions about the positions can be sent to us. For more information about the chair MAIS, please visit our web site.
A post-doctoral position on program analysis and verification is open at University of Paris Diderot (Paris 7) for joining the Modeling and Verification group at LIAFA. The position is open for one year, starting no later than mid-2016. If the position is taken before the end of 2015, it could be prolonged for a second year. The salary is competitive and includes health insurance.
The position is funded by the french ANR project Vecolib: Verifying Automatically the Correct Use and Implementation of Container Libraries. The project addresses foundational and practical issues related to the following topics:
Candidates must have a PhD in computer science, and be skilled in both theoretical and practical aspects. They must have a solid background in theory (automata, logics, algorithms, etc.) and a practical experience in software development. Experience with software development, for example verification/analysis tool prototypes, is very welcome. We are seeking individuals who are self-motivated and autonomous, willing to take initiatives in research. Good English or French language skills are mandatory.
Interested candidates may send further questions and a short statement of research interests, including their CV and two or three reference persons to Mihaela Sighireanu or any member of the group (Ahmed Bouajjani, Constantin Enea or Peter Habermehl).
Applications are invited for a post-doctoral research position in the Computational Logic Center at the University of Iowa in the area of interactive theorem proving and verification.
The position is funded by DARPA through the HACMS program. The work will be done in collaboration with researchers at New York University, the Université Paris Sud and Princeton University. The main goal of the project is to increase the level of automation in the Coq proof assistant by soundly integrating SMT solvers into it. Our immediate emphasis is on supporting software verification efforts by other research groups currently funded by HACMS. However, we expect that the results of the integration will benefit Coq users in general.
The ideal candidate will have a Ph.D. in Computer Science, general knowledge of formal methods, and expertise in interactive theorem proving in higher-order logics, with substantial experience in using Coq, Isabelle, or similar tools. Candidates should demonstrate strong programming and formal modeling skills. Previous experience in writing Coq tactics and plug-ins is a considerable plus. Familiarity with SMT is welcome but not required.
The position is a full time appointment that runs initially through August 2016 and could be renewed for another year subject to satisfactory performance and continuous availability of funds. Review of applications will begin immediately. The position will remain open until filled. The start date is negotiable, but ideally it should be as soon as possible. The starting salary is $56,000 per year, plus health and vacation benefits.
There might be also be a possibility to teach one course in the spring semester in the Computer Science department as a visiting assistant professor. This is, however, a separate position that would entail a corresponding reduction of effort for the postdoc appointment. It should be understood as an opportunity, not as a requirement for the postdoc contract.
Inquiries and applications should be sent via email to Cesare Tinelli with "Coq postdoc" in the subject. When sending an application please include your CV together with a brief description of your research accomplishments and interests, including the names of three references.
The department of Information Technology, Uppsala University, opens two fully paid PhD student positions in Computer Science, on formal specification and verification for concurrent systems. One position will focus on verification and correctness proofs of programs, and the other will focus on semantics and specification languages. Advisors are Tjark Weber and Joachim Parrow.
The positions are fully paid for 5 years and include 20% teaching duties. The work will be carried out in the Modeling of Concurrent Computation research group http://www.it.uu.se/research/group/mobility
The candidate should have a Master of Science in Computer Science, Computer Engineering, Mathematics or equivalent, with a strong background in logic, formal semantics and concurrent/parallel programming. Experience with interactive theorem proving (e.g., Isabelle, Coq) is a plus. Good knowledge of written and spoken English is a requirement for employment.
For more details and instructions on how to apply see the position description. For more information on what support you can expect see our web page.
Rigorous System Design team at Verimag research lab in Grenoble is recruiting a PhD student motivated for solving practical research problems of programming many-core systems while satisfying real-time constraints. We consider industrial case studies from avionics and spacecraft domains and target state-of-the-art multi-core platforms.
Though the real-time systems research offers efficient schedulability algorithms, their practical use encounters serious challenges:
The first challenge concerns with the lack of formal development techniques for software-intensive systems with real-time constraints. Our work is based on an expressive formal programming and modeling framework BIP, providing refinement, code generation and verification of functional and timing properties for embedded systems. The PhD candidate is expected to develop BIP runtimes and code generation tools for multi-cores, extending our previous work in [1].
The next primary challenge is mixed criticality. The traditional static safety-critical scheduling has to be extended by mixed-critical scheduling, which re-shapes the schedulability analyses in a non-trivial way. The candidate is expected to extend our scheduling algorithms and tools [2] to take into account a set of multi-core platform constraints and evaluate them in different application case studies.
The last but not the least, the conservative timing analysis is a challenging problem, involving two major aspects: the execution time uncertainty in multi-path programs and on cache/bus/network interference between different tasks. The candidate is expected to adapt our statistical model-checking techniques [3] to the analysis of execution times and interferences in real-time multi-core systems.
Our research lab is located in the Grenoble area, one of the world's most prominent research and technology areas, hosting researchers from all over the world, but also known for its tourism attractions due to nearby spa, ski, alpinism, and other facilities in the heart of the picturesque French Rhône-Alps.
The interested candidates are invited to contact Prof. Dr. Saddek Bensalem, University of Grenoble Alpes, and Dr. Marius Bozga, CNRS.
References:
[1] A Timed-automata based Middleware for Time-critical Multi-core Applications. D. Socci, P. Poplavko, P. Bourgos, S. Bensalem and M. Bozga, In Proc. SEUS 2015.
[2] Multiprocessor Scheduling of Precedence-constrained Mixed-Critical Jobs. D. Socci, P. Poplavko, S. Bensalem, M. Bozga. In Proc. ISORC-2015.
[3] Building Faithful High-level Models and Performance Evaluation of Manycore Embedded Systems. A. Nouri, M. Bozga, A. Molnos, A. Legay and S. Bensalem. In Proc. MEMOCODE-2014.
Two fully-funded PhD studentships are currently available in the School of Science & Engineering at the University of Dundee. These cover the students' tuition fees (at the UK/EU rate) and provide a stipend for living expenses. Very strong candidates who are interested in studying for a PhD in areas aligned to the Computing research strengths of the School are encouraged to apply. Candidates should have a 1st class degree or a Masters degree (or equivalent) in a relevant subject.
Suitable topics include but are not limited to: Human-Centred Computing, Argumentation Technology, Graph Theory, Artificial Intelligence, Programming Languages, Space Technology, Real-time graphics and visualisation, Computer Vision and Biomedical Image Analysis.
Detailed information about our research is available by following links to the various research groups on our web site. Specific examples of possible PhD project topics and information on how to apply can be found on the web site.
Candidates are encouraged to apply as soon as possible. Initial enquiries (including a detailed CV and a statement of interest) are welcomed and should be made to the prospective supervisor.
If only there was a place where I could prove theorems for money, change the world, and have fun while doing it...
Sounds too good to be true?
In the Trustworthy Systems team, that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities.
We are looking for multiple motivated entry-level proof engineers who want to join our team, move things forward, and have global impact. We are expanding our team, because seL4 is going places. There are active projects around the world in automotive, aviation, connected consumer devices, SCADA, and spaceflight. To make these projects successful, we need to scale formal verification. You
The salary range for this position is AUD 65,000 to 90,000 for recent graduates, depending on experience and qualification. See the NICTA web site for details.
Since my first CADE, in 2009, I have always looked forward to the next installment with trepidation. This year was no exception: The jubilee edition in Berlin was extremely stimulating, with an unusually high number of participants, invited speakers, workshops, tutorials, and competitions. The program chairs and local organizers deserve our warmest congratulations for managing such a successful event.
The conference this year was undeniably under the sign of Vampire. Andrei Voronkov was an invited speaker, he received the Herbrand award, he coauthored two regular papers at CADE, and he co-organized the Vampire workshop. His presentations are always as entertaining as insightful. And we should all heed to his warning:
Do not try to immitate my career. You will end up in a completely random place.[general laughter] I'm serious.
We were told that Vampire's new architecture, AVATAR, works like a well-run couple. The AVATAR couple consists of a SAT solver and a first-order (FO) module. (Unlike Andrei, I will stay 100% politically correct in this column and avoid assigning genders to SAT and FO in this column. Use your imagination.) The key to AVATAR is that the SAT solver bosses the FO prover around, not the other way. In this respect, Vampire's architecture is not entirely dissimilar from an SMT solver.
Geoff Sutcliffe delivered a talk about "Things You Can't Do with a Vampire". Here is my addendum:
Does there exist a function f from reals to reals such that for all x and y, f(x + y * y) - f(x) >= y?
Your tasks:
Before you start working on these tasks, make sure to solve Larry Wos's puzzles first. I would not want to steal customers from him.
If this is any indication of the difficulty of the task, it took me about one hour to solve Point 1; an M.Sc. student of mine also needed one hour; and a colleague who holds two Ph.D.s was able to solve it in half an hour (or is a liar). Point 2 is a research problem, I believe. If you have a solution, I would like to hear from you. The reader with the best solution will receive an awesome trophy from me and see their name and solution printed in the next installment of this newsletter.