LEADER 04297nam  22006975  450 
001 9910483590903321
005 20251225173603.0
010   $a3-030-68446-6
024 7 $a10.1007/978-3-030-68446-4
035   $a(CKB)4100000011763231
035   $a(DE-He213)978-3-030-68446-4
035   $a(MiAaPQ)EBC6478487
035   $a(PPN)25385850X
035   $a(EXLCZ)994100000011763231
100   $a20210212d2021      u|         0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt$2rdacontent
182   $cc$2rdamedia
183   $acr$2rdacarrier
200 10$aLogic-Based Program Synthesis and Transformation $e30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7?9, 2020, Proceedings /$fedited by Maribel Fernández
205   $a1st ed. 2021.
210  1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2021.
215   $a1 online resource (X, 345 p. 64 illus., 1 illus. in color.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12561
311 08$a3-030-68445-8 
320   $aIncludes bibliographical references and index.
327   $aRewriting -- Symbolic Computation in Maude: Some Tapas (Invited Paper) -- Runtime Complexity Analysis of Logically Constrained Rewriting -- Con uence and Commutation for Nominal Rewriting Systems with Atom Variables -- Pattern eliminating transformations -- Unification -- Nominal Uni cation with Letrec and Environment-Variables -- Terminating Non-Disjoint Combined Unification -- Types -- slepice: Towards a Verified Implementation of Type Theory in Type Theory -- Resourceful Program Synthesis from Graded Linear Types -- Verification -- On Constrained Horn Clauses and Program Veri cation (Invited Paper) -- Algorithm Selection for Dynamic Symbolic Execution: a Preliminary Study -- Translation of Interactive Datalog Programs for Microcontrollers to Finite State Machines -- Model Checking and Probabilistic Programming -- Generating Functions for Probabilistic Programs -- Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs -- Program Analysis and Testing -- Testing Your (Static Analysis) Truths -- Slicing unconditional jumps with unnecessary control dependencies -- Logics -- A Formal Model for a Linear Time Correctness Condition of Proof Nets of Multiplicative Linear Logic -- Synthesis of Modality De nitions and a Theorem Prover for Epistemic Intuitionistic Logic.
330   $aThis book constitutes the refereed proceedings of the 30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020, which was held during September 7-9, 2020. The 15 papers presented in this volume were carefully reviewed and selected from a total of 31 submissions. The book also contains two invited talks in full paper length. The contributions were organized in topical sections named: rewriting; unification; types; verification; model checking and probabilistic programming; program analysis and testing; and logics.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12561
606   $aComputer science
606   $aArtificial intelligence
606   $aSoftware engineering
606   $aMachine theory
606   $aComputer engineering
606   $aComputer networks
606   $aComputer Science Logic and Foundations of Programming
606   $aArtificial Intelligence
606   $aSoftware Engineering
606   $aFormal Languages and Automata Theory
606   $aComputer Engineering and Networks
615  0$aComputer science.
615  0$aArtificial intelligence.
615  0$aSoftware engineering.
615  0$aMachine theory.
615  0$aComputer engineering.
615  0$aComputer networks.
615 14$aComputer Science Logic and Foundations of Programming.
615 24$aArtificial Intelligence.
615 24$aSoftware Engineering.
615 24$aFormal Languages and Automata Theory.
615 24$aComputer Engineering and Networks.
676   $a004.015113
702   $aFerna?ndez$b Maribel
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910483590903321
996   $aLogic-Based Program Synthesis and Transformation$92914320
997   $aUNINA