Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 0911.3440

Proceedings International Workshop on Verification of Infinite-State Systems

Axel Legay
View original source ↗Read source document ↗Export metadata ↓

Abstract

This volume contains the proceedings of the 11th International Workshop on Verification of Infinite-State Systems (INFINITY 2009). The workshop was held in Bologna, Italy on August 31, 2009, as a satellite event to the 20th International Conference on Concurrency Theory (CONCUR 2009). The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.

Explore related subjects

cs.LOcs.DMcs.FL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Axel Legay. 2009-11-17. Proceedings International Workshop on Verification of Infinite-State Systems. https://doi.org/10.4204/eptcs.10

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both come with different modalities. In the logical semantics, formulas are interpreted in a world of a Kripke model but given a history of prior announcements and receptions that already happened. An axiomatisation AA for such a logic has been given in prior work, for the formulas that are valid when interpreted in the Kripke model before any such announcements have taken place. This axiomatisation is a reduction system wherein one can show that every formula is equivalent to a purely epistemic formula without dynamic modalities for announcements and receptions. We propose a generalisation AA* of this axiomatisation, for the formulas that are valid when interpreted in the Kripke model given any history of prior announcements and receptions of announcements. It does not extend the axiomatisation AA, for example it is no longer valid that nobody has received any message. Unlike AA, this axiomatisation AA* is infinitary and it is not a reduction system.

cs.LO↗
arXiv2026

Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA

This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance of primo is achieved by a systematic literature survey, repeated profiling, and parameter tuning. The resulting solver outperforms the winner of the QF-LRA track of SMT-COMP~2026. This confirms that vibe-coding of automated reasoning tools will enable us to make great strides in the future.

cs.LO↗