Symbolic computation in automated program reasoning

DOI10.1007/978-3-031-27481-7_1zbMath1529.68080OpenAlexW4323026993MaRDI QIDQ6174522

Laura Kovács

Publication date: 17 August 2023

Published in: Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-27481-7_1

zbMATH Keywords

symbolic computationformal methodsprobabilistic reasoningloop analysisalgebraic recurrences

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A unified approach for studying the properties of transition systems
• On the hardness of analyzing probabilistic programs
• Aligator.jl -- a Julia package for loop invariant generation
• Computing the algebraic relations of \(C\)-finite sequences and multisequences
• Invariant Generation for Multi-Path Loops with Polynomial Assignments
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Aligator: A Mathematica Package for Invariant Generation (System Description)
• Automatic Generation of Polynomial Loop Invariants
• Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences
• Continuous Reasoning
• Polynomial Invariants for Affine Programs
• Reasoning Algebraically About P-Solvable Loops
• An axiomatic basis for computer programming
• Solving invariant generation for unsolvable loops

This page was built for publication: Symbolic computation in automated program reasoning