Symbolic computation in automated program reasoning

DOI10.1007/978-3-031-27481-7_1MaRDI QIDQ6174522zbMATH OpenOpenAlexFDO

Authors 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

algebraic recurrencesformal methodsloop analysisprobabilistic reasoningsymbolic computation

Mathematics Subject Classification ID

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

Recommendations

• Reasoning in symbolic computation
• Symbolic computing
• Towards specifying symbolic computation
• Symbolic computation via program transformation
• Symbolic methods and automata
• scientific article; zbMATH DE number 1140679
• scientific article; zbMATH DE number 1538926

Cites work

• A unified approach for studying the properties of transition systems
• Aligator: A Mathematica Package for Invariant Generation (System Description)
• Aligator.jl -- a Julia package for loop invariant generation
• An axiomatic basis for computer programming
• Automated generation of non-linear loop invariants utilizing hypergeometric sequences
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Automatic Generation of Polynomial Loop Invariants
• Computing the algebraic relations of \(C\)-finite sequences and multisequences
• Continuous reasoning: scaling the impact of formal methods
• Handbook of automated reasoning. In 2 vols
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Invariant generation for multi-path loops with polynomial assignments
• On the hardness of analyzing probabilistic programs
• Polynomial Invariants for Affine Programs
• Reasoning Algebraically About P-Solvable Loops
• Solving invariant generation for unsolvable loops

Cited in

(6)

• Symbolic evaluation with structural recursive symbolic constants
• Programming and symbolic computation in Maude
• Programming and automating mathematics in the Tarski-Kleene hierarchy
• Automated programming, symbolic computation, machine learning: my personal view
• Exact and approximate moment derivation for probabilistic loops with non-polynomial assignments
• Symbolic techniques in satisfiability solving

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174522)