I have been asked, sometimes by students, about how research can proceed. Indeed, if memory serves, I once had a course taught by Reinhold Baer on how research progresses.
In this column, I plan to give some insights of my own. Of course, research is risky, often resulting in no visible and useful product. But the journey can be exciting; it certainly has been many times for me. And, occasionally, gold is found: a new proof, a shorter proof, and, that jewel, an answer to an open question.
Two main types of research occur immediately: study of a new approach -- strategy, inference rule, representation, for example -- or study of an area of mathematics or logic that you have not studied before. Or you may simply wish to explain how research sometimes occurs, expounding on the source of new ideas.
Here, I shall offer an area of mathematics for research, an area whose answer is currently unknown, from what I have been told. I shall put forth some notions, in part based on my own years of study in automated reasoning, mathematics, and logic. (Of course, my goal is to inspire research that culminates in effective procedures that I can then use to find new proofs, shorter proofs, and new theorems.) I offer four illustrations leading respectively to the set of support strategy, the demodulation procedure, the inference rule of paramodulation, and the weighting strategy.
Those new to the field of automated reasoning may not be familiar with this part of history; others may just enjoy the retelling of true stories. The illustrations I offer are chosen because, individually and collectively , the discoveries featured have proved invaluable in the use of an automated reasoning program to successfully answer open questions from areas of mathematics and logic.
The year is 1963. The place is Argonne National Laboratory. The
individual who provided the needed force is Dan Carson. The object is to
find a proof of a simple theorem in group theory, namely, in groups of
exponent 2, which asserts that the square of every element x is the
identity e, commutativity can be proved. The obstacle is that
too many conclusions are drawn and retained for the program to complete
a proof.
Carson, discouraged, says gloomily: the program runs out of memory.
I ask for some time to think about a solution.
Thirty-two minutes later Carson calls to say the game is up.
I suggest that he try what would be called eventually the set of
support strategy: For this theorem, have the program draw conclusions
recursively from xx = e and the denial of commutativity, ab != ba;
that is, prevent the program from applying binary resolution to pairs of
clauses both of which are among the axioms for a group.
Yes, a proof was found, and found quickly, and a strategy was formulated
that has since become a mainstay of theorem proving.
I also find it interesting that
different users have different views about the content of the initial
set of support.
Some recommend including the negation of the goal that is sought, while
others prefer a proof that is not bidirectional.
Aphorism: For a new program, new approach, or new strategy, choose a simple theorem that has resisted proof, and see whether, with the new idea, a proof is found. But be careful that your method is general.
The year is 1967. The place again is Argonne National Laboratory. The
object this time is to find a proof of a trivial lemma that will in turn
be used to prove that the square root of 2 is irrational. The obstacle
is the retention of too many clauses before memory is exhausted.
Yes, the situation sounds familiar, but the solution was not.
The approach was to read some 2,000 clauses in the hope that some
key property of the clauses would be discovered.
Our first conjecture was that many of the 2,000 clauses were trivial,
such as 0 + a + 0 = a for the constant a present in the denial.
That conjecture was proved wrong: only about 39 of the 2,000 were
trivial in the sense just illustrated.
Our next conjecture was that if these clauses were not retained, their
removal would result in a huge reduction in their offspring.
Such indeed was the case.
The solution was to add a list in the input that would "demodulate" such
clauses to something that subsumption would take care of, something like 0 + x = x as a subsumer.
In other words, canonicalize and simplify deduced conclusions with rules
of the type just given or with rules such as associativity.
All went well.
Demodulation was thus formulated and, eventually, used for various other
purposes including finding shorter proofs.
I also use it for avoiding the use of various lemmas that are deemed
undesirable.
Yes, sometimes a logician or mathematician wishes to see whether a proof
can be found that is simpler than already known, where simpler means
avoiding various lemmas or avoiding certain types of term.
What often varies from researcher to researcher is which demodulators to
include.
Aphorism: Read the output of retained conclusions when an objective is not reached. Doing so can help you identify useless information.
The year is 1968. The place -- you guessed it -- is Argonne National Laboratory. The object is to address a need, posed by Alan Robinson in a paper for what was then called automated theorem proving, to cope with equality in a manner far better than how all relations were coped with; meaning was not used. In other words, treat equality as if it were understood. Perhaps because of the formulation of demodulation, the notion was to (in effect) generalize the basics of demodulation by permitting unification to go both ways -- to allow, when needed, unification in both an argument of equality and in the term in focus. Paramodulation was born; but, fortunately, George Robinson pointed out that nonunit clauses containing the key equality should be included, rather than merely focusing on unit equalities. Paramodulation has proved most useful. Robert Veroff states that virtually all of his research focusing on proof finding relies on paramodulation.
Aphorism: Accept challenges offered by people with a good track record.
The year is 1971. This time the place is Northern Illinois University. The object is to find a way to increase the efficiency of programs when seeking to find proofs. The approach, introduced by Ross Overbeek, was to circumscribe the terms considered essential for finding the sought-after proof and avoid clauses with (so-to-speak) undesirable terms. Weighting was born, and for many years it was used successfully to instruct a program about the relative desirability of various terms. My own view of weighting differs slightly in that I consider its main function to be advice-giving. By assigning low weights to various expressions, I cause the program to prefer conclusions containing corresponding subterms. Regardless of which view you take, however, weighting remains an important strategy for directing the program's reasoning.
Aphorism: Think hard, formulate a means that appears to meet the objective, and don't be afraid to experiment with or adapt an idea. The danger to avoid is having too limited a focus.
Now I close with the promised area for research, namely, lattice theory, featured in my last column.
Where "v" denotes union or join and "^" denotes intersection or meet, William McCune found two 29-letter single axioms, the following.
(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (w v ((v6 v x) ^ (x v v7))) = x. (((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (((w v x) ^ (v6 v x)) v v7) = x.
The proposed research focuses on two open questions. (1) Does there exist a shorter single axiom for lattice theory in terms of meet and join? (2) In terms of meet and join, how long is the shortest single axiom for lattice theory? The (nonstandard) 4-basis McCune chose as target was the following.
y v (x^ (y^z)) = y y^ (x v (y v z)) = y ((x^y) v (y^z)) v y = y ((x v y)^ (y v z))^y = y
The properties of associativity for union and intersection in the 6-basis that follows present obstacles that require, ordinarily, too much CPU time to overcome. Nevertheless, if you would enjoy research focusing on the 6-basis and, particularly, on the difficulties offered by associativity, I offer the following basis.
y ^ x = x ^ y (x ^ y) ^ z = x ^ (y ^ z) y v x = x v y (x v y) v z = x v (y v z) x ^ (x v y) = x x v (x ^ y) = x
Attempting to answer an open question is obviously quite challenging, but that activity is so stimulating.
An election was held from October 12 to November 15 2018 to fill two positions on the board of trustees of CADE, Inc.
Four candidates were nominated (in alphabetic order): Christoph Benzmüller, Aart Middeldorp, Stephan Schulz, and Geoff Sutcliffe.
Following the decision at the IJCAR business meeting this year, participants of the last three CADE or IJCAR conferences were invited to vote, and a total of 270 ballots were sent by electronic mail on October 12. 57 valid ballots were returned, which translates to a participation rate of 21.1% (as compared to 9.1% in 2017, 11.2% in 2016, 11.0% in 2015, 10.0% in 2014, 11.8% in 2013, 13.0% in 2012, 16.2% in 2011).
The 2 candidates elected are Stephan Schulz and Christoph Benzmüller.
The counting of the votes according to the single transferable vote algorithm described in the CADE Bylaws is detailed near the end of this newsletter.
After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:
On behalf of the AAR and CADE Inc., I thank Aart Middeldorp for his service on the board of trustees since 2015.
Stephan Schulz is joining the board as new elected member, but was also serving as ex-officio trustee for IJCAR 2018, so we would like to thank him for the continuing service on the board.
I would also like to thank Geoff Sutcliffe for running in the election, and for his invaluable help with the AAR and CADE web presence!
Congratulations to Christoph Benzmüller and Stephan Schulz on being (re)elected!
The Steering Committee of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods ("TABLEAUX") currently has three elected members whose terms will expire:
The Steering Committee is therefore calling for nominations of candidates who wish to contest an election for three positions, which will be held in December 2018.
To nominate please send an email to Jens Otten (jeotten@ifi.uio.no) containing:
Only members of the TABLEAUX community may act as nominators and a person may nominate or second only one candidate. Closing date for nominations is December 22nd 2018.
The TABLEAUX community consists of all people who have been registered participants in at least one of the three most recent TABLEAUX Conferences including IJCAR (i.e. IJCAR 2016, TABLEAUX 2017 and IJCAR 2018) and all members of the current IJCAR Program Committee.
The current Steering Committee rules and more information can be found on the TABLEAUX website.
Homotopy Type Theory is a young research area combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory and higher category theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. These ideas have led to many interesting developments, from the study of syntax and semantics of type theories to practical formalizations in proof assistants based on univalent type theory.
The HoTT/UF workshops, co-located with FSCD since 2016, started out as a forum for formalization of mathematics in a univalent setting. From the 2017 edition and onwards, its scope has been broadened to
Special Issue
We are soliciting submissions for a Special Issue of the journal
Submission is open and contributions will be reviewed on a *rolling basis*, as soon as they are received. Accepted papers will be published on the MSCS website via 'FirstView' and will be citeable through a DOI shortly after acceptance - before the completion of the whole journal issue (expected end of 2019). Submission will be closed on December 31, 2018.
For details and submission instructions see the special issue web page.
Relational and algebraic methods belong to the core of computer science. This special issue aims to showcase the variety and relevance of recent developments in this field ranging from theory to applications.
We invite submissions of high-quality original research articles in the general fields of algebras relevant to computer science and applications of such algebras. Topics include but are not limited to:
While we welcome substantially extended versions of papers published in the proceedings of the RAMiCS 2018 conference (Springer LNCS 11194), this call is open to anyone interested in the field of relational and algebraic methods.
Important Dates:
Information about the submission instructions and more details is available on the full call for papers.
The term “imprecise probability” (IP for short) usually refers to a family of models that provide a description of phenomena for which incomplete or imprecise information has been advanced, overcoming the limitations of traditional models of uncertainty based on precise probabilities. The basic idea of IP models is to extend the standard theory of precise probabilities by considering sets of traditional models. From this perspective the uncertainty (beliefs) of an agent about the possible states of the world is for instance modelled by sets of probabilities rather than a single one. Extensions include, among others, lower and upper previsions, belief functions, sets of desirable gambles and partial preference orderings.
IP is strongly linked with another framework where to express, study and reason on forms of imprecision and incompleteness: logic. Indeed, on the one hand standard logic methodologies have been applied to characterise and study IP notions such as coherence and models in terms of lower and upper probabilities/expectations. On the other hand concepts stemming from the IP tradition have been used to formulate appropriate semantics for statistical relational languages (e.g. by enabling to go beyond limitations such as cyclicity in probabilistic logic programs), whereas viewing IP as an abstract logic structure has lead to its application to domains such as for instance quantum mechanics, sum-of-square optimisation and classical logic itself.
This Special Issue intends to contribute to the state-of-the-art of the interactions and connections between imprecise probabilities and logic, and more generally with formal theories of rationality, the hope being that this cross-disciplinary view will lead to new exciting perspectives for both communities and related areas.
Topics
Topics of interests include but are not limited to the following:
Submission Instructions
All submitted papers under this call will undergo the standard review
process of the journal.
Submission Period
Mar 1st, 2019 - Jun 1st, 2019
All papers should be submitted to IJAR website by choosing the Special Issue “VSI:Imprecise probabilities, logic and rationality”.
All online submissions should follow the “Guide for Authors” of the journal.
Modern society is increasingly dependent on software systems that are becoming larger and more complex. This poses new challenges to the various aspects of software engineering, for instance, software dependability in trusted computing, interaction with physical components in cyber physical systems, distribution in cloud computing applications, security and privacy in general. Hence, new concepts and methodologies are required to enhance the development of software engineering from theoretical aspects. TASE 2019 aims to provide a forum for people from academia and industry to communicate their latest results on innovative advances in software engineering. The authors of a selected subset of accepted papers will be invited to submit extended versions of their papers to a special issue of the Science of Computer Programs journal.
Topics
The symposium is devoted to theoretical aspects of software engineering. Topics of interest include, but are not limited to:
Important Dates
For more information see the conference website.
It is now more than 30 years since the first VDM symposium in 1987 brought together researchers with the common goal of creating methods to produce high quality software based on rigour and reason. Since then the diversity and complexity of computer technology has changed enormously and the formal methods community has stepped up to the challenges those changes brought by adapting, generalising and improving the models and analysis techniques that were the focus of that first symposium. The theme for FM 2019 is a reflection on how far the community has come and the lessons we can learn for understanding and developing the best software for future technologies.
Topics of Interest:<\ br> FM 2019 encourages submissions on formal methods in a wide range of domains including software, computer-based systems, systems-of-systems, cyber-physical systems, human-computer interaction, manufacturing, sustainability, energy, transport, smart cities, and healthcare. We particularly welcome papers on techniques, tools and experiences in interdisciplinary settings. We also welcome papers on experiences of formal methods in industry, and on the design and validation of formal methods tools. The broad topics of interest for FM 2019 include, but are not limited to:
Important Dates:
For more information see the conference website.
FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, models of computation (e.g. quantum computing, probabilistic computing, homotopy type theory), semantics and verification in new challenging areas (e.g. blockchain protocols or deep learning algorithms).
Suggested, but not exclusive, list of topics for submission are:
Important Dates
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
For more information see the conference website.
CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including foundations, applications, implementations, theoretical results, practical experiences and user studies are solicited.
At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award.
Important Dates:
For more information, see the conference website.
CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration.
CICM 2018 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to
Important Dates:
More information on the conference website.
The 26th edition of the SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software, but does not exclude analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, and empirical evaluation.
Topics of interest include, but are not limited to:
SPIN 2019 will be organized as an ACM SIGSOFT event, colocated with the International Symposium on Software Testing and Analysis (ISSTA 2019).
Important Dates:
More information on the conference website.
CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science.
Topics of Interest
Typical, but not exclusive topics of interest are:
Important Dates
More information (types of submissions, submission process...) available on the conference website.
FroCoS (Symposium on Frontiers of Combining Systems) and TABLEAUX (Conference on Automated Reasoning with Analytic Tableaux and Related Methods) are two of the main conferences on the theory and application of logical systems. Their 2019 edition will be hosted by the Middlesex University in London, from 3 to 6 September 2019. In keeping with the tradition of the two events, we invite proposals for colocated workshops and tutorials on all topics related to logical reasoning: from theoretical aspects, to applications, to tools for interactive or automated reasoning. Workshops and tutorials can target the logical systems community in general, or alternatively focus on a particular system, recent theoretical development or application.
Colocated events will take place on 2 and 3 September 2019 (before the start of the conference programs) and will be held on the same premises as the main conferences. Workshop/tutorial-only attendees will enjoy a significantly reduced registration fee.
Detailed matters such as paper submission and review process, or publication of proceedings, are up to the organizers of individual events. All accepted workshops and tutorials will be expected to have their program ready by 10 August 2019.
Proposals for workshops and tutorials should contain at least the following pieces of information:
Proposals are invited to be submitted by email to chair@frocos2019.org and chair@tableaux2019.org, no later than 1 February 2019. Selected events will be notified by 9 February 2019. The workshop/tutorial selection committee consists of the FroCoS and TABLEAUX program chairs and the conference organizers.
FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis. Starting in 2000, the conference proceedings have been published in Springer's LNCS/LNAI series. FroCoS 2019 will be co-located with the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019). The two conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions.
Scope of Conference
In various areas of computer science, such as logic,
computation, program development and verification, artificial intelligence, knowledge representation,
and automated reasoning, there is an obvious need for using specialized formalisms and
inference systems for selected tasks. To be usable in practice, these specialized systems must
be combined with each other and integrated into general purpose systems. This has led to the
development of techniques and methods for the combination and integration of dedicated formal
systems, as well as for their modularization and analysis. FroCoS traditionally focuses on these types
of research questions and activities.
Like its predecessors, FroCoS 2019 offers a
forum for research in the general area of combination, modularization, and integration of systems,
with emphasis on logic-based methods.
Topics of interest
Important Dates
For more information, please visit the conference website.
TABLEAUX is the main international conference at which research on all aspects — theoretical foundations, implementation techniques, systems development and applications — of the mechanization of tableaux-based reasoning and related methods is presented. TABLEAUX has been held every year since 1992. Starting in 1995, the proceedings have been published in Springer's LNCS/LNAI series. TABLEAUX 2019 will be co-located with the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019). The two conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions
Scope of Conference
Tableau methods offer a convenient and flexible set of tools for automated
reasoning in classical logic, extensions of classical logic, and non-classical
logics. Areas
of application include verification of software and computer systems,
deductive databases, knowledge representation and its required inference engines, teaching,
and system diagnosis.
Topics of interest include but are not limited to:
We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the tableau community, and should focus on the role of reasoning and on logical aspects of the solution.
Important Dates
For more information, please visit the conference website.
Since 1969, the ARITH symposia have served as the flagship conference for presenting scientific work on the latest research in computer arithmetic. Computer arithmetic is now driving the most important innovations and product directions in our industry, such as artificial intelligence and security.
Authors are invited to submit papers describing recent advances on all aspects related to computer arithmetic, its applications or implementations. This includes, but is not restricted to, the following topics:
Important dates
More information on the symposium website.
This workshop aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE), on the topic of Horn clause based analysis, verification and synthesis.
Horn clauses have been advocated by these communities at different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.
Aims and Scope
Topics of interest include but are not limited to the use of Horn
clauses, constraints, and related formalisms in the following areas:
We solicit regular papers describing theory and implementation of Horn-clause-based analysis and tool descriptions. We also solicit extended abstracts describing work-in-progress, as well as presentations covering previously published results that are of interest to the workshop.
CHC-COMP
HCVS 2019 will host the 2nd CHC competition (CHC-COMP), which will
compare state-of-the-art tools for CHC solving for performance and
effectiveness on a set of publicly available benchmarks.
More information can be found here.
All participants of CHC-COMP are invited (but not obliged) to submit
a tool description for publishing either online or at the proceedings
through the EasyChair system for HCVS (the HCVS deadlines apply).
Important dates
More information on the workshop website.
Just before and after the main WoLLIC 2019 event, Utrecht University will host two satellite workshops:
Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are:
Important Dates
For more information, see the workshop web page.
The VMCAI school is meant to facilitate interaction, cross-fertilization, and advancement of hybrid methods that combine Verification, Model Checking, Abstract Interpretation, etc.
A detailed program is available at the school website.
Registration:
The registration deadline for the winter school is December 22, 2018.
The registration is *free* but it is mandatory. Please take into
consideration that the number of attendees is limited. Register
as soon you are sure to be able to attend the Winter School.
More details are available at the school website.
A 12-month position for post-doctoral research on Symbolic tools for the formal verification of cryptographic protocols is available at the Inria Nancy / LORIA research center within the Inria project team PESTO: Proof techniques for security protocols as part of the ERC Grant SPOOC: Automated Security Proofs of Cryptographic Protocols.
Security protocols are distributed programs that aim at ensuring security properties, such as confidentiality, authentication or anonymity, by the means of cryptography. Such protocols are widely deployed, e.g., for electronic commerce on the Internet, in banking networks, mobile phones and more recently electronic elections. As properties need to be ensured, even if the protocol is executed over untrusted networks (such as the Internet), these protocols have shown extremely difficult to get right. Formal methods have shown very useful to detect errors and ensure their correctness.
One generally distinguishes two families of security properties: trace properties and observational equivalence properties. Trace properties verify a predicate on a given trace and are typically used to express authentication properties. Observational equivalence expresses that an adversary cannot distinguish two situations and is used to model anonymity and strong confidentiality properties.
The Tamarin prover is a state-of-the art protocol verification tool which has recently been extended to verify equivalence properties in addition to trace properties. SAPIC allows protocols to be specified in a high-level protocol specification language, an extension of the applied pi-calculus, and uses the Tamarin prover as a backend by compiling the language into multi-set rewrite rules, the input format of Tamarin. Tamarin and SAPIC have been successfully used to verify standards such as TLS 1.3 and 5G AKA as well as industrial protocols such as OPC UA. The objective of this postdoc is to contribute to the development of the SAPIC/Tamarin toolchain, work on extensions and use the tool(s) to analyse particular classes of protocols.
Successful candidates must have defended a PhD in computer science, or expect to defend their PhD before taking up the position. Expected qualifications are:
Contacts:
The position is located at the Inria Nancy / LORIA research center in Nancy, France, with over 430 researchers, engineers and technicians. Nancy is a young (more than 45,000 students) city in eastern France with a rich cultural life and a high quality of life. It is famous for its UNESCO World Heritage Site "Place Stanislas". Paris is only 1h30 by TGV, Luxembourg, Germany and the Vosges mountains less than 1h30 by car.
Applications, including
should be sent to the the addresses indicated above as two pdf files (one for the publications, the other for the other documents).
Additionally, at least one recommendation letter from your PhD advisor(s), and up to two additional letters of recommendation should be sent directly by their authors to the email addresses indicated above.
Applications should be received by June 30, 2019, but applications received later may still be considered.
Informal enquiries concerning the position are welcome.
The Department of Computer Science at Aarhus University is looking for excellent and visionary tenure track Assistant Professors or Associate Professors to push the frontiers of Computer Science research. Aarhus University - an international top-100 University - has made an ambitious strategic investment in a 5-year recruitment plan to radically expand the Department of Computer Science.
Applicants within all areas of computer science are welcome, including Programming Languages, Software Engineering, Logic and Semantics.
The application deadline is January 6th 2019.
Additional details and instructions on how to apply are found here.
The College of Computing and Informatics (CCI) at Drexel University is uniquely positioned to become a research and education leader for the 21st century. With a commitment to expand the college and grow the faculty in key areas of strength, CCI seeks candidates with intellectual curiosity, as well as, innovative knowledge to help drive cutting edge research, teaching and curriculum design.
CCI invites applications for multiple tenure-track and tenured faculty positions in Computer Science at all levels. Candidates should have a Ph.D. in Computer Science or related field at the time of appointment and a record of high-quality scholarly activities. Applicants for senior hires are expected to have demonstrated exceptional leadership in large-scale, multidisciplinary research programs. Preference will be given to applicants in the areas of Artificial Intelligence, Data Science, Machine Learning, and Privacy/Security.
Drexel is a private university committed to research with real-world applications. The university has over 25,000 students in 14 colleges and schools and offers about 200 degree programs. The College of Computing and Informatics has over 60 faculty, close to 2,000 students and 15 academic programs. Drexel has one of the largest and best known cooperative education programs in the country, with over 1600 co-op employers. Drexel is located on Philadelphia's "Avenue of Technology" in the University City District and at the hub of the academic, cultural, and historical resources of the nation's fifth largest metropolitan region.
Successful applicants will be expected to teach at the undergraduate and graduate levels, establish strong sponsored research programs, advise undergraduate and graduate students, and be involved in service to the college, the university, as well as the global academic community.
Application Instructions
Evaluation of applications will be conducted on a rolling basis; however, applicants should apply by January 15, 2019 for full consideration.
Applications should include a cover letter, CV, letters of reference, and brief statements describing the applicant's research program and teaching interests. Electronic submissions in PDF format are required.
Drexel University is an Equal Opportunity/Affirmative Action Employer. The College of Computing & Informatics is especially interested in qualified candidates who can contribute to the diversity and excellence of the academic community. Background investigations are required for all new hires as a condition of employment, after the job offer is made. Employment will be contingent upon the University's acceptance of the results of the background investigation.
The Chairs of Information Security and Programming Methodology at ETH Zurich are recruiting PhD students and post-docs for a project on formal verification of secure networked systems.
The Chairs of Information Security and Programming Methodology at ETH Zurich are recruiting PhD students and post-docs for a project on formal verification of secure networked systems. The project’s focus will be on verifying the protocols and implementation for a secure Future Internet architecture. Details are available online here and here.
Key requirements for successful applications:
Applications and questions should be sent to David Basin and Peter Müller. The application should include a CV, a description of research interests, a transcript of grades for Ph.D. student applicants, and optionally theses or publications. We will consider applications until the positions are filled. The start date is negotiable.
More details about the positions:
2 PostDoc positions are available in my group at Inria Paris on the F* and ERC SECOMP projects. I am seeking exceptional candidates with a strong, internationally competitive research track record.
On F*, I am looking for someone with research expertise in: programming language semantics, dependent types, type theory, effects, monads, mechanized metatheory, functional programming, formal verification. Here is a (non-exhaustive) list of potential research topics on which we could work.
On ERC SECOMP, I am particularly looking for someone with expertise in:
Candidates are expected to work collaboratively on project-relevant topics and help advise students, but can also dedicate some of their time to their own independent projects. For exceptional candidates with enough experience we can also discuss about Starting Researcher positions, who can propose and follow their own research agenda and be fairly independent. Our team can also support such exceptional candidates for permanent Researcher positions funded and awarded competitively by Inria. Further details about these various positions are available here.
Do not hesitate to contact me if you are interested in joining the team!
I am pleased to announce the availability of multiple postdoc and PhD student positions in my research group at the Max Planck Institute for Software Systems (MPI-SWS), funded by a 2015 ERC Consolidator Grant for the project "RustBelt: Logical Foundations for the Future of Safe Systems Programming".
This 5-year project (which began in April 2016) concerns the development of rigorous formal foundations for the Rust programming language. The project summary appears at the bottom of this message.
Although the main high-level goal of the project is to build logical foundations for the Rust programming language -- see our POPL'18 paper -- the project also serves to fund technical work on two other major research efforts that feed into the main goal:
Postdocs:
I am seeking exceptional candidates with a strong,
internationally competitive track record of research in programming
languages and/or verification. The primary criterion is quality, but
I am particularly interested in candidates who have specialized
expertise in one or more of the following areas:
Students:
I am seeking exceptional candidates who have at least some
background in programming language theory and/or formal methods, and
who are eager to work on deep foundational problems with the potential
for direct impact on a real, actively developed language. A
bachelor's or master's degree is required. For more details about the
MPI-SWS graduate program, see here.
Applications will be considering until the end of the year. If you are interested in joining the RustBelt team and want to learn more about the project, please contact Derek Dreyer directly. To apply for a postdoc (or PhD student) position, please submit a CV (and/or grade transcript), research statement (or statement of purpose), and list of references here. If you are unable to apply by the deadline but are interested in a position, please contact Derek Dreyer anyway.
For further information, see the project web page.
Multiple Postdoc Positions on Verification and Security Analysis for Hypervisor and Block Chain at Nanyang Technological University.
We have several exciting research projects on
The postdoc will work in the Cyber-Security Laboratory at Nanyang Technological University using theorem proving technologies.
The position involves conducting basic research, developing tools, working as part of a large research team, travelling, and giving presentations. The working language is English.
Apart from specific requirement to the topic a general candidate requirement are:
The term is currently one to three years starting immediately. The salary is 5.5k to 7k SGD per month with up to 4 month performance bonus. (Singapore Tax is around 5%)
Interested applicants should send their CV to Dr. David Sanan.
Candidates must be experienced on one or more of the following areas:
We are are hiring again!
If only there were a place where I could prove theorems for money, change the world, and have fun while doing it...
Sounds too good to exist?
In the Trustworthy Systems team at Data61 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 proof engineers who want to join our team in Sydney, move things forward, and have global impact. You would
To apply for this position, you should possess a significant subset of the following skills.
We are hiring at two levels, so if you are more qualified or experienced than the above would suggest, you can come in as a senior proof engineer.
If you additionally have experience
If you have the right skills and background, we can provide training on the job. Continual learning is a central component of everything we do. You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements.
We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See here for more information.
Salary ranges, in AUD (plus superannuation):
Apply online at the following link for the Proof Engineer positions:
Your application should include a cover letter, CV, undergraduate transcript (if applicable), and contact information for two references.
This round of applications closes on 17 December 2018.
For any questions on these positions, please contact Rafal Kolanski.
The seL4 code and proof are open source. Check them out.
More information about Data61's Trustworthy Systems team here.
There are additional proof engineering positions available on the Cogent project. Cogent is a language we designed to ease the verification of systems components around seL4. For expressions of interest, see contact details.
Looking to do a PhD? Data61 and UNSW offer scholarships! See here for details.
We are looking for a full-time research scientist in formal verification to join us, the Trustworthy Systems group, at Data61, CSIRO. 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.
Our vision is a world in which computer users can choose all three: correct, secure, and fast. We believe that most current approaches to building systems are fundamentally flawed. We aim to demonstrate a better way. Our approach is rooted in foundational, formal verification using theorem provers (e.g., Isabelle, HOL4), and high-performance system design. If you find this vision appealing, and have ideas about how to pursue it, we want to hear from you.
Our team brings together a unique combination of expertise in systems, security, formal verification, and programming languages. We are the creators of seL4, the world's first operating system microkernel with a machine-checked proof (in Isabelle/HOL). seL4 boasts both extreme performance and foundational binary-level correctness and security proofs. We are also involved in CakeML, the most realistic verified compiler for a functional programming language, and a promising approach to scaling full verification up to applications code.
We are building on these successes in various directions, including concurrency (formal reasoning and implementation), timing (real-time guarantees and timing channels), and whole-system verification using component systems (e.g., CAmKES) and code+proof co-generation.
We publish in top conferences, and are involved in multiple international research collaborations. You will have the opportunity to teach at UNSW should you wish to take it. We have a flexible, friendly, and intellectually stimulating work environment.
We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See here for more information.
The salary range for this position (plus superannuation) is
Apply online here.
Your application should include a cover letter, CV, short research statement, and contact information for two references.
This round of applications closes on 15 January 2019.
For any questions on this position, please contact June Andronic.
I am looking to recruit someone who has experience of writing proof tactics in HOL and/or is experienced in using Z3 in order to accelerate D-RisQ’s product development of independent code verification. Proof tactic development would be done using ProofPower Z but we have expertise within D-RisQ to help a recruit familiar with one of the other HOL implementations work with ProofPower and Z.
Lean Forward is an ambitious research project that aims at formally proving theorems in research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles, by collaborating with number theorists. The project is funded by an NWO Vidi grant from January 2019 to December 2023 and is hosted by the Vrije Universiteit Amsterdam.
We will use Lean, an exciting new proof assistant developed at Microsoft Research (Leonardo de Moura) and Carnegie Mellon (Jeremy Avigad). Lean draws on decades of experience in interactive and automatic theorem provers, including Coq, Isabelle, and Z3. Its logic is very expressive, and emphasis is placed on strong proof automation. The system is easy to extend via metaprograms that rely on the same logical language that is used to express specifications and proofs.
As part of this project, we will develop formal libraries of fundamental number theory and explore how to automate proof search in these. Moreover, we will develop techniques and tools that help mathematicians perform accurate computations and reasoning using proof assistants, integrating procedures from computer algebra systems in a foundational, verified fashion. The ultimate aim is to develop a proof assistant that actually helps mathematicians by making them more productive and more confident in their results.
We are looking for outstanding candidates for several fully funded, four-year PhD positions, due to start in 2019 or early 2020. Candidates should ideally have some experience with (automatic or interactive) theorem proving or mathematics and be at ease with both theory and engineering. Please contact Jasmin Blanchette for more information.
Applications are invited for up to ten fully-funded PhD studentships in the School of Computer Science at the University of Nottingham, starting on 1 October 2019.
The topics for the studentships are open, but should relate to one of the School’s research groups: Agents Lab; Automated Scheduling and Planning; Computer Vision Lab; Data Driven Algorithms, Systems and Design; Functional Programming Lab; Intelligent Modelling and Analysis; Uncertainty in Data and Decision Making; Mixed Reality Lab.
The studentships are for a minimum of three years and include a stipend of £14,777 per year and tuition fees. They are open to students of any nationality. Applicants are normally expected to have a first-class MSc or BSc in Computer Science or a related discipline, and must obtain the support of a supervisor in the School prior to submitting their application. Initial contact with supervisors should be made at least two weeks prior to the closing date for applications. Informal enquiries may be addressed here.
To apply, please submit the following items by email to Christine Fletcher:
Closing date for applications: Friday 18 January 2019
Applicants in the area of the Functional Programming Laboratory are strongly encouraged! If you are interested in applying, please contact a potential supervisor at least two weeks prior to the 18th January deadline:
We are seeking to appoint a PhD student in UCL’s Programming Principles, Logic, and Verification (PPLV) group,to work alongside the EPSRC-funded project “A coalgebraic framework for reductive logic and proof-search (ReLiC)”.
The project is led by David Pym (PI), Alexandra Silva, and Simon Docherty (Co-Is). Facebook (Peter O’Hearn) is a partner in the project.
The position is available from 23 September 2019 for 4 years. The starting stipend will be approximately £17,280, with an approximate annual uplift of 3%.
We are looking for a talented, highly motivated student interested in working on some aspects of the project. Here is a description of the project.
The traditional treatment of logic is that of a deductive science: from axioms, conclusions are deduced according to formal proof rules. However, in practice many applications of logic and mathematical reasoning proceed in the opposite direction: from a putative conclusion, one finds sufficient axioms from which it may be concluded. This proceeds not by a step-by-step application of proof rules, but instead by the systematic reduction of the space of possible (deductive) proofs. We call this the reductive approach to logic. Archetypal examples of reductive reasoning in computer science include automated theorem proving, logic programming languages such as PROLOG, and precondition inference in program verification.
The ReLiC project aims to produce a uniform mathematical foundation for reductive logic via the framework of coalgebra and coinduction. Coalgebra can fruitfully be seen as a unifying formalism for stateful systems, while coinduction is a closely connected proof principle based on the reduction of goals into subgoals. In doing so we aim to
We are looking for a student with an excellent first degree in mathematics, computer science, philosophy, or another mathematical discipline, who has a strong background and interest in logic. Ideally, candidates will also have an excellent, relevant Master’s degree and strong programming skills.
For an informal discussion of the position, please contact David, Alexandra, or Simon.
To apply, please follow the instructions here and indicate clearly on your application that you are applying for this Scholarship ("A Coalgebraic framework for reductive logic and proof-search") under the scholarships section, or in your personal statement.
1-3 Postdoc positions in formal methods are available at the Department of Informatics, University of Oslo. The positions are for 3 years. Application deadline 13 January 2019.
The official announcement can be found here.
Please get in touch with Einar Broch Johnsen for more information.
Topics
The successful applicants are expected to contribute to ongoing research activities in the group, including:
The positions are funded by Sirius, a Centre for Research-Driven Innovation (SFI) at the University of Oslo. It constitutes a long-term interdisciplinary research initiative, funded by the Research Council of Norway, involving both academic research teams (UiO, NTNU and Oxford University) as well as industrial partners including operators (Equinor), service companies (Schlumberger and DNV GL) and IT companies (e.g., Computas, Evry, IBM).
The successful applicant should have an interest in working on real industrial problems in collaboration with industrial partners, as well as on basic research problems. The candidate will be expected to contribute to on-going activities in the group, such as:
Expected Background
The candidate should have expertise in one or more of the following areas:
The candidate should have implementation experience and programming skills in these fields. The candidate should have a strong publication record. Experience in research collaboration with industry, international mobility, and international collaborations is an advantage.
Competitive Salary and Environment
The Computer Science department of the University Koblenz-Landau (Campus Koblenz) invites applications for the position of a Research Assistant (wissenschaftlicher Mitarbeiter/Mitarbeiterin, 1,0 EGr. 13 TV-L) at PhD level, in the research groups Formal methods and theoretical computer science (Prof. Dr. Viorica Sofronie-Stokkermans) and Computer Networks (Prof. Dr. Hannes Frey).
The application deadline is January 31, 2019.
Additional details and instructions on how to apply can be found here.
Informal enquiries are welcome and may be sent to Viorica Sofronie-Stokkermans.
An election was held to fill 2 positions. Christoph Benzmüller, Aart Middeldorp, Stephan Schulz, and Geoff Sutcliffe were nominated. 57 valid ballots were returned. Therefore, in each iteration of the single transferable vote algorithm described in the CADE Bylaws, a candidate is elected if she or he gets at least 29 first preference votes. Otherwise, the votes of the candidate with the least first preference votes are redistributed.
The following table reports the initial distribution of preferences among the candidates:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | no supp. |
| Christoph Benzmüller | 17 | 11 | 15 | 12 | 2 |
| Aart Middeldorp | 17 | 8 | 9 | 21 | 2 |
| Stephan Schulz | 15 | 17 | 18 | 6 | 1 |
| Geoff Sutcliffe | 8 | 21 | 13 | 12 | 3 |
By redistributing the votes of Geoff Sutcliffe, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Christoph Benzmüller | 19 | 17 | 19 | 2 |
| Aart Middeldorp | 19 | 13 | 23 | 2 |
| Stephan Schulz | 19 | 25 | 12 | 1 |
By redistributing the votes of Aart Middeldorp, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Christoph Benzmüller | 26 | 29 | 2 |
| Stephan Schulz | 31 | 25 | 1 |
To find the next elected candidate, we redistribute the votes of Stephan Schulz and get the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Christoph Benzmüller | 20 | 22 | 13 | 2 |
| Aart Middeldorp | 21 | 10 | 24 | 2 |
| Geoff Sutcliffe | 16 | 24 | 14 | 3 |
By redistributing the votes of Geoff Sutcliffe, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Christoph Benzmüller | 29 | 26 | 2 |
| Aart Middeldorp | 27 | 28 | 2 |
To summarize, the 2 candidates elected are Stephan Schulz and Christoph Benzmüller.
A few days before I am done with editing an issue of the newsletter, I often receive an email that start with "I have heard that the next AAR newsletter will soon be published..." or something similar. It also happens that sometimes such an email comes a bit too late for me to include the information in the newsletter.
I realize that, since there is no fixed schedule, people that organize events such as conferences and can't anticipate if they have a chance to publish their CfP (or any other information) in the next AAR newsletter can easily be taken by surprise. To remedy that, I am considering creating a mailing list for people that want to know a few weeks in advance when the next newsletter will appear. If you would be interested in such a thing let me know. I'll see if it is worth creating such a list depending on the number of people interested.
* * *
A few days ago, I discovered this paper by Luca Aceto that talks about what it is that researchers in universities are doing.
I found this text on the mark, easy of access and also quite funny, which made me want to talk about it here. The end of the year festivities are an opportunity to catch up with people you don't see often. This year, I am definitely going to use this reference if the question of what I do at work comes up in the discussion!
* * *
Happy end of the year festivities and holidays to all AAR members