scientific article; zbMATH DE number 7269249

zbMath1490.68134arXiv1811.02133MaRDI QIDQ5129945

Ugo Dal Lago, Naoki Kobayashi, Charles Grellois

Publication date: 3 November 2020

Full work available at URL: https://arxiv.org/abs/1811.02133

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

model checkingprobabilistic programshigher-order programstermination probabilities

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

On higher-order reachability games vs may reachability ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• MoCHi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Branching-time model-checking of probabilistic pushdown automata
• Probabilistic encryption
• On probabilistic term rewriting
• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Design and analysis of randomized algorithms. Introduction to design paradigms.
• On the \(\lambda Y\) calculus
• Analyzing probabilistic pushdown automata
• The IO and OI hierarchies revisited
• Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable
• Recursive Markov Decision Processes and Recursive Stochastic Games
• Probabilistic Termination
• Environmental bisimulations for probabilistic higher-order languages
• Probabilistic operational semantics for the lambda calculus
• Finitary Semantics of Linear Logic and Higher-Order Model-Checking
• On the Hardness of Almost–Sure Termination
• Model Checking of Recursive Probabilistic Systems
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Probabilistic Termination by Monadic Affine Sized Typing
• Krivine Machines and Higher-Order Schemes
• COMPUTING LEAST FIXED POINTS OF PROBABILISTIC SYSTEMS OF POLYNOMIALS
• Recursion Schemes and the WMSO+U Logic
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Probabilistic Automata on Finite Words: Decidable and Undecidable Problems
• Handbook of Model Checking
• Compositional higher-order model checking via ω -regular games over Böhm trees
• Semantics for probabilistic programming
• Types and higher-order recursion schemes for verification of higher-order programs
• Relational semantics of linear logic and higher-order model-checking
• Collapsible Pushdown Automata and Recursion Schemes
• Stochastic invariants for probabilistic termination
• Model Checking Higher-Order Programs
• A type-directed abstraction refinement approach to higher-order model checking
• On coinductive equivalences for higher-order probabilistic functional programs
• Probabilistic coherence spaces are fully abstract for probabilistic PCF
• On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi
• Probabilistic Turing Machines and Computability
• Term Rewriting and Applications
• Probabilistic game semantics
• Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
• CONCUR 2005 – Concurrency Theory