- Centre National de la Recherche ScientifiqueFR528 papers
- University of ViennaAT480 papers
- Vienna Center for Quantum Science and TechnologyAT328 papers
- Commissariat à l'Énergie Atomique et aux Énergies AlternativesFR275 papers
- European Organization for Nuclear ResearchCH263 papers
- Charles UniversityCZ245 papers
- ETH ZurichCH223 papers
- Institute of High Energy PhysicsCN223 papers
- Université Paris-SaclayFR219 papers
- CEA Paris-SaclayFR215 papers
- University of WarsawPL215 papers
- Massachusetts Institute of TechnologyUS209 papers
7 papers · 2 filters
Temporal Logic as Filtering
Alena Rodionova, Ezio Bartocci, Dejan Nickovic +1
We show that metric temporal logic can be viewed as linear time-invariant filtering, by interpreting addition, multiplication, and their neutral elements, over the (max,min,0,1) id…
The QBF Gallery: Behind the Scenes
Florian Lonsing, Martina Seidl, Allen Van Gelder
Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successf…
Automated Benchmarking of Incremental SAT and QBF Solvers
Uwe Egly, Florian Lonsing, Johannes Oetsch
Incremental SAT and QBF solving potentially yields improvements when sequences of related formulas are solved. An incremental application is usually tailored towards some specific…
Efficient computation of generalized Ising polynomials on graphs with fixed clique-width
Tomer Kotek, Johann A. Makowsky
Graph polynomials which are definable in Monadic Second Order Logic (MSOL) on the vocabulary of graphs are Fixed-Parameter Tractable (FPT) with respect to clique-width. In contrast…
Model Checking Tap Withdrawal in C. Elegans
Md. Ariful Islam, Richard DeFrancisco, Chuchu Fan +3
We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW…
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Florian Lonsing, Uwe Egly
We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API to allow for incr…