AAR Newsletter

Author: jcailler

aarnewsletter.html

@@ -167,9 +167,9 @@ <h1><a href="http://www.aarinc.org/">
     <div class="issue">
       Newsletter No. 146<br />January 2025</div>
 
-    <div>
+    <div id="div-toc">
       <ul class="toc">
-         <li><a href="#herbrand">Herbrand Award 2025: Call for Nominations</a></li>
+        <li><a href="#herbrand">Herbrand Award 2025: Call for Nominations</a></li>
         <li><a href="#mccune">Bill McCune PhD Award in Automated Reasoning 2025</a></li>
         <li><a href="#grant_title">Grant Proposals</a>
           <ul>
@@ -185,20 +185,26 @@ <h1><a href="http://www.aarinc.org/">
         <li><a href="#conferences-title">Conferences</a>
           <ul>
             <li><a href="#TYPES2025">TYPES 2025: 31st International Conference on Types for Proofs and Programs</a></li>
-           <li><a href="#SAT2025">SAT 2025: 28th International Conference on Theory and Applications of Satisfiability
+            <li><a href="#SAT2025">SAT 2025: 28th International Conference on Theory and Applications of Satisfiability
                 Testing</a></li>
             <li><a href="#TbiLLC2025">TbiLLC 2025: 15th International Tbilisi Symposium on Logic, Language, and
                 Computation</a></li>
-            <li><a href="#MFPS41">MFPS XLI: 41st Conference on Mathematical Foundations of Programming Semantics</a></li>
+            <li><a href="#MFPS41">MFPS XLI: 41st Conference on Mathematical Foundations of Programming Semantics</a>
+            </li>
+            <li><a href="#FMCAD25">FMCAD 2025: 25th International Conference on Formal Methods in Computer-Aided
+                Design</a>
+            </li>
             <li><a href="#CICM2025">CICM 2025: 18th Conference on Intelligent Computer Mathematics and LSFA 2025: 20th
                 International Symposium on Logical and Semantic Frameworks, with Applications, call for papers</a></li>
             <li><a href="#ECAI2025">ECAI-2025: 28th European Conference on Artificial Intelligence</a></li>
-            <li><a href="#RuleML+RR 2025">RuleML+RR 2025: 9th International Joint Conference on Rules and Reasoning</a></li>
+            <li><a href="#RuleML+RR 2025">RuleML+RR 2025: 9th International Joint Conference on Rules and Reasoning</a>
+            </li>
           </ul>
         </li>
         <li><a href="#workshops_title">Workshops</a>
           <ul>
-            <li><a href="#VSS2025">VSS 2025: First International Workshop on Verification of Scientific Software</a></li>
+            <li><a href="#VSS2025">VSS 2025: First International Workshop on Verification of Scientific Software</a>
+            </li>
             <li><a href="#FMBC2025">FMBC 2025: 6th International Workshop on Formal Methods for Blockchains</a></li>
             <li><a href="#pmfm2025">Workshop in Programs from Proofs Meets Formal Mathematics</a></li>
           </ul>
@@ -215,14 +221,17 @@ <h1><a href="http://www.aarinc.org/">
         </li>
         <li><a href="#open_positions_title">Open Positions</a>
           <ul>
-            <li><a href="#APMonterey">Faculty Associate - Research of Computer Science, Naval Postgraduate School, Monterey,
+            <li><a href="#APMonterey">Faculty Associate - Research of Computer Science, Naval Postgraduate School,
+                Monterey,
                 CA </a></li>
-            <li><a href="#PhDSheffield">PhD Position on Model Checking of Functional Programs at University of Sheffield, UK
+            <li><a href="#PhDSheffield">PhD Position on Model Checking of Functional Programs at University of
+                Sheffield, UK
               </a></li>
             <li><a href="#PhDLondon">PhD Studentship at UCL Computer Science, UK</a></li>
             <li><a href="#PhDSouthCarolina">Two PhD Positions at the Computer Science and Engineering Department at the
                 University of South Carolina, USA</a></li>
-            <li><a href="#PhDETH">Two PhD Positions in Formal Semantics and Verification (with a focus on Rust) at ETH Zürich,
+            <li><a href="#PhDETH">Two PhD Positions in Formal Semantics and Verification (with a focus on Rust) at ETH
+                Zürich,
                 Switzerland</a></li>
             <li><a href="#PDSpain">Several Postdoctoral Positions on Formal Methods for Security and Privacy at the
                 Universitat Rovira i Virgili, Spain </a></li>
@@ -837,6 +846,75 @@ <h3 id="MFPS41"><a href="https://coalg.org/calco-mfps-2025/mfps/">MFPS XLI: 41st
         </p>
       </div>
 
+      <div id="conf-FMCAD">
+        <h3 id="FMCAD25"><a href="https://fmcad.org/FMCAD25/">FMCAD 2025: 25th International Conference on Formal
+            Methods in Computer-Aided Design</a>, call for papers</h3>
+        <div class="details">October 6-10, 2025, SRI Headquarters, Menlo Park, CA, US</div>
+        <p>
+          FMCAD 2025 is the twenty-fifth edition in a series of conferences on the theory and
+          applications of formal methods in hardware and system verification. The conference
+          encompasses a wide range of topics related to formal aspects of computer-aided system
+          design, including verification, specification, synthesis, and testing and provides
+          a leading forum to researchers in academia and industry for presenting and discussing
+          groundbreaking methods, technologies, theoretical results, and tools for reasoning
+          formally about computing systems.
+        </p>
+
+        <p>
+          FMCAD 2025 includes the <a href="https://fmcad.org/FMCAD25/student_forum/">FMCAD Student Forum</a>
+          and is co-located with VSTTE 2025.
+        </p>
+
+        <p>
+          FMCAD welcomes submission of papers reporting original research on advances in all
+          aspects of formal methods and their applications to computer-aided design.
+          Topics of interest include (but are not restricted to):
+        <ul>
+          <li>Model checking, theorem proving, equivalence checking, abstraction and reduction, compositional methods,
+            decision
+            procedures at the bit- and word-level, probabilistic methods, combinations of deductive methods and decision
+            procedures.</li>
+          <li>Synthesis and compilation for computer system descriptions, modeling, specification, and implementation
+            languages,
+            formal semantics of languages and their subsets, model-based design, design derivation and transformation,
+            correct-by-construction methods.</li>
+          <li>Application of formal and semi-formal methods to functional and non-functional specification and
+            validation of
+            hardware and software, including timing and power modeling, verification of computing systems on all levels
+            of
+            abstraction, system-level design and verification for embedded systems, cyber-physical systems, automotive
+            systems
+            and other safety-critical systems, hardware-software co-design and verification, and transaction-level
+            verification.
+          </li>
+          <li>Experience with the application of formal and semi-formal methods to industrial-scale designs; tools that
+            represent formal verification enablement, introduce new features, or substantially improve the automation of
+            formal
+            methods.</li>
+          <li>Application of formal methods to verifying safety, connectivity and security properties of networks,
+            distributed
+            systems, smart contracts, block chains, and IoT devices.</li>
+          <li>Application of formal methods to the analysis of machine learning systems, and applications of machine
+            learning to
+            enhance formal methods techniques.</li>
+        </ul>
+        </p>
+
+        <p>
+          <b>Important Dates (AoE):</b><br />
+        <ul>
+          <li>Abstract Submission Deadline: April 20, 2025</li>
+          <li>Paper Submission Deadline: April 27, 2025</li>
+          <li>Author Response: June 17 - June 19, 2025</li>
+          <li>Author Notification: July 1, 2025</li>
+        </ul>
+
+        </p>
+
+        <p>More information is available on the conference's <a href="https://fmcad.org/FMCAD25/">web page</a>.
+        </p>
+      </div>
+
       <div id="conf-CICM">
         <h3 id="CICM2025"><a href="https://cicm-conference.org/2025">CICM 2025: 18th Conference on Intelligent
             Computer
@@ -854,7 +932,7 @@ <h3 id="CICM2025"><a href="https://cicm-conference.org/2025">CICM 2025: 18th Con
           soliciting formal CICM submissions there will be associated workshops with
           separate submission options.
         </p>
-      
+
         <p>
           Topics of interest include (but are not restricted to):
         <ul>
@@ -863,7 +941,7 @@ <h3 id="CICM2025"><a href="https://cicm-conference.org/2025">CICM 2025: 18th Con
           <li>digital mathematical libraries</li>
         </ul>
         </p>
-      
+
         <p>
           <b>Important Dates (AoE):</b><br />
         <ul>
@@ -875,28 +953,29 @@ <h3 id="CICM2025"><a href="https://cicm-conference.org/2025">CICM 2025: 18th Con
           <li>Camera-ready copies due: July 18, 2025</li>
         </ul>
         </p>
-      
+
         <h4>20th International Symposium on Logical and Semantic Frameworks, with Applications</h4>
-      
+
         <p>
-          LFSA 2025 is a satellite event of CICM 2025. LSFA is an International Symposium on Logical and Semantic Frameworks
-          with Applications launched in 2006. Logical and
+          LFSA 2025 is a satellite event of CICM 2025. LSFA is an International Symposium on Logical and Semantic
+          Frameworks with Applications launched in 2006. Logical and
           semantic frameworks are formal languages that represent logics and languages, as well as computational, AI and
           deductive
-          systems. These frameworks provide mathematical foundations for the formal specification of systems and programming
+          systems. These frameworks provide mathematical foundations for the formal specification of systems and
+          programming
           languages, supporting tool development and reasoning.
         </p>
-      
+
         <p>
-          The LSFA series is a platform that fosters collaboration, bringing together theoreticians and practitioners. LSFA
-          aims
+          The LSFA series is a platform that fosters collaboration, bringing together theoreticians and practitioners.
+          LSFA aims
           to promote techniques and results from the theoretical side, ranging from well-established ones such as lambda
           calculus
-          and type theory to state-of-the-art ones such as machine learning, and provide feedback on integrating, implementing
-          and
+          and type theory to state-of-the-art ones such as machine learning, and provide feedback on integrating,
+          implementing and
           using such methods and results from the practical side.
         </p>
-      
+
         <p>
           <b>Important Dates (AoE):</b><br />
         <ul>
@@ -906,8 +985,8 @@ <h4>20th International Symposium on Logical and Semantic Frameworks, with Applic
           <li>Camera-ready copies due: July 18, 2025</li>
         </ul>
         </p>
-      
-      
+
+
         <p>More information is available on <a href="https://cicm-conference.org/2025">CICM 2025</a> and <a
             href="https://lsfa-workshop.github.io/2025/index.html">LSFA 2025</a> web pages.
         </p>
@@ -1039,6 +1118,8 @@ <h3 id="RuleML+RR 2025"><a href="https://2025.declarativeai.net/events/ruleml-rr
             href="https://2025.declarativeai.net/events/ruleml-rr">web page</a>.
         </p>
       </div>
+
+
     </div>
 
     <div id="workshops">
@@ -1537,7 +1618,8 @@ <h3 id="PhDSouthCarolina">Two PhD Positions at the Computer
         </p>
 
         <p>
-          Interested candidates are encouraged to contact <a href="mailto:[email protected]">Frank (Peng) Fu</a> directly. The
+          Interested candidates are encouraged to contact <a href="mailto:[email protected]">Frank (Peng) Fu</a> directly.
+          The
           application deadline for Fall 2025 is <b>February 1, 2025</b>.
         </p>
 
@@ -1562,7 +1644,8 @@ <h3 id="PhDETH">Two PhD Positions in Formal Semantics and Verification (with a f
         </p>
 
         <p>
-          Interested candidates should send an email to <a href="mailto:[email protected]">Refl Jung</a>. Please explain
+          Interested candidates should send an email to <a href="mailto:[email protected]">Refl Jung</a>. Please
+          explain
           why you are interested in a PhD in this field and what your prior experience is. Also include a CV and
           possible contacts for recommendation letters. Applications are
           considered on a rolling basis, so there is no fixed end date for this call, but if you want to be sure the
@@ -1641,7 +1724,8 @@ <h3 id="IntershipVirginia">Internship at Virginia Tech's Systems Software Resear
         </p>
 
         <p>
-          The starting date and time frame is flexible. Please contact <a href="mailto:[email protected]">Swarn Priya</a> with a
+          The starting date and time frame is flexible. Please contact <a href="mailto:[email protected]">Swarn Priya</a>
+          with a
           resume or for any questions.
         </p>
 
@@ -1675,7 +1759,8 @@ <h3 id="APLIRMM">Associate Professor Position at LIRMM, Montpellier, France</h3>
         </p>
 
         <p>
-          Please contact please contact <a href="mailto:[email protected]">Abdelhak-Djamel Seriai</a> (head of the MaREL team)
+          Please contact please contact <a href="mailto:[email protected]">Abdelhak-Djamel Seriai</a> (head of the MaREL
+          team)
           if
           you want more information about the application's process.
         </p>
@@ -1751,40 +1836,46 @@ <h3 id="PDSurrey">Research Fellow in Verification or Security or Concurrent/Dist
 
         <p>
           The application deadline for applicants is <b>January 31st, 2025</b>. You can apply on the <a
-            href="http://jobs.surrey.ac.uk/048824-R">University's web site</a>. For informal enquiries and further
+            href="http://jobs.surrey.ac.uk/048824-R">University's web page</a>. For informal enquiries and further
           information please contact <a href="mailto:[email protected]">Brijesh Dongol</a> or <a
             href="mailto:[email protected]">Gregory Chockler</a>.
         </p>
       </div>
 
       <div id="job-ULB">
-        <h3 id="PPULB">Full-time Academic Position in Computer Science at Université libre de Bruxelles (ULB), Belgium</h3>
+        <h3 id="PPULB">Full-time Academic Position in Computer Science at Université libre de Bruxelles (ULB), Belgium
+        </h3>
 
         <p>
           The Faculty of Sciences of the Université libre de Bruxelles (ULB) invites applications for a full-time
-          academic position in Computer Science to begin October 1st, 2025. All areas of Computer Science will be considered. Candidates who can strengthen an existing team within our department
+          academic position in Computer Science to begin October 1st, 2025. All areas of Computer Science will be
+          considered. Candidates who can strengthen an existing team within our department
           are particularly encouraged to apply.
         </p>
 
         <p>
-          The Computer Science Department of ULB is a leading research and dynamic education center. Located in the capital of
-          Europe, it offers a wide range of funding and research opportunities. Brussels is a cosmopolitan city with an excellent
-          quality of life and easy access to all major cities in Europe. The position involves both teaching and research and some
+          The Computer Science Department of ULB is a leading research and dynamic education center. Located in the
+          capital of
+          Europe, it offers a wide range of funding and research opportunities. Brussels is a cosmopolitan city with an
+          excellent
+          quality of life and easy access to all major cities in Europe. The position involves both teaching and
+          research and some
           commitment to administrative tasks.
         </p>
 
         <p>
           For more information, (e.g. concerning courses to be taught or the research carried out in the
-          Department), please contact <a href="mailto:[email protected]">Mr John Jacono</a>, Head of the Computer Science Department.
+          Department), please contact <a href="mailto:[email protected]">Mr John Jacono</a>, Head of the Computer
+          Science Department.
         </p>
 
         <p>
           The application deadline for applicants is <b>March 15, 2025</b>. You can apply on the <a
-            href="https://cwfront.ulb.ac.be/greffe/modules/vac/data/sources/pdf/prod/8889.pdf">University's web site</a>.
+            href="https://cwfront.ulb.ac.be/greffe/modules/vac/data/sources/pdf/prod/8889.pdf">University's web
+            page</a>.
         </p>
       </div>
 
-
       <div id="job-cryspen">
         <h3 id="cryspen">Proof Engineer at Cryspen, France and Germany</h3>