Journal of Logical and Algebraic Methods in Programming

Article	Citations
Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic	12
Multifaceted formal methods and their interdisciplinary role — From the cathedral of ‘components as coalgebras’ to the HCI context and the open source software bazaar	11
Exception-sensitive program slicing	11
ElixirST: A session-based type system for Elixir modules	10
Generation of algebraic data type values using evolutionary algorithms	10
Decomposing monolithic processes in a process algebra with multi-actions	8
Editorial Board	8
Bunch theory: Axioms, logic, applications and model	7
Editorial Board	7
Maude2Lean: Theorem proving for Maude specifications using Lean	7
Efficient analysis of belief properties in process algebra	6
On the inner structure of multirelations	6
Bounded model checking of multitask PLC ST programs with preemption using rewriting modulo SMT	6
Compositional separation of control flow and data flow	6
An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis	5
Fair termination of multiparty sessions	5
First order Büchi automata and their application to verification of LTL specifications	5
Hoare-style logic for unstructured programs	5
Plotkin's call-by-value λ-calculus as a modal calculus	5
Verification of the ROS NavFn planner using executable specification languages	5
Editorial Board	5
Time distance-based computation of the DBM over-approximation of preemptive real-time systems	5
Composition of synchronous communicating systems	4
From symbolic constraint automata to Promela	4
A model of systems with modes and mode transitions	4

A dynamic logic with branching modalities	4
Unified opinion formation analysis in rewriting logic	4
An algebraic theory of nondeterministic finite automata	4
Back to the format: A survey on SOS for probabilistic processes	4
A type language for distributed reactive components governed by communication protocols	4
Logic and Calculi for All on the occasion of Luís Barbosa’s 60th birthday	4
Relation-changing models meet paraconsistency	4
Expressive power and succinctness of the positive calculus of binary relations	3
Advancing orchestration synthesis for contract automata	3
Program equivalence in a typed probabilistic call-by-need functional language	3
Trace preservation in B and Event-B refinements	3
Rule and constraint based debugging of DBpedia queries	3
Capturing constrained constructor patterns in matching logic	3
A generic construction for crossovers of graph-like structures and its realization in the Eclipse Modeling Framework	3
Open compliance in multiparty sessions with partial typing	3
Verification of mutable linear data structures and iterator-based algorithms in Dafny	3
Semantics of quantum programming languages: Classical control, quantum control	3
Program slicing of Java programs	3
CRYSTAL framework: Cybersecurity assurance for cyber-physical systems	3
Session-based concurrency in Maude: Executable semantics and type checking	2
Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models	2
A distribution semantics for probabilistic term rewriting	2
Safe orchestrated multicomposition of systems of communicating finite state machines	2
Inferring RPO symbol orderings	2
Comodule representations of second-order functionals	2
A memory-related vulnerability detection approach based on vulnerability model with Petri Net	2
Editorial message from the new Editor-in-Chief	2
Probabilistic mediator: A coalgebraic perspective	2
A generalized concurrent rule construction for double-pushout rewriting: Generalized concurrency theorem and language-preserving rule applications	2
Counterpart-based Quantified Temporal Logics	2
Formal models for consent-based privacy	2
Formal analysis of the application programming interface of the PVS verification system	2
Monadic second-order incorrectness logic for GP 2	2
Editorial Board	2
Verification of time-bounded multiset rewriting properties	2
Preface to selected papers from 21st Workshop on Programming and Languages (PROLE 2022)	2
Editorial Board	2
Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications	2
A formal framework for distributed cyber-physical systems	2
Location automata for synchronised shuffle expressions	2
Monitorable hyperproperties of nonterminating systems	2
Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting	2
Towards refinable choreographies	2
Algebraic reasoning for timeliness-guided system design	1
Formalization of the inverse kinematics of three-fingered dexterous hand	1
Axiomatizing recursion-free, regular monitors	1
Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification	1
Hypergraph Lambek grammars	1
A formal framework for security testing of automotive over-the-air update systems	1
Formalizing CCS and π-calculus in Guarded Cubical Agda	1

Weighted automata extraction and explanation of recurrent neural networks for natural language tasks	1
An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency	1
A lightweight approach to smart contracts supporting safety, security, and privacy	1
Program equivalence in an untyped, call-by-value functional language with uncurried functions	1
Unification and anti-unification in applicative matching logic	1
Journal of Logical and Algebraic Methods in Programming – Publisher's Note 2025	1
Realizability modulo theories	1
Editorial Board	1
bGSL: An imperative language for specification and refinement of backtracking programs	1
Preface of the PLACES 2023 special issue	1
Coherent modal transition systems refinement	1
DM-Check: Verifying invariants of concurrent systems by deductive model checking	1
A framework for formal verification of robot kinematics	1
Quantum encoding of dynamic directed graphs	1
Editorial Board	1
A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems	1
On difunctions	1
Editorial Board	1
Secure information flow connections	1
Editorial Board	1
On proving that an unsafe controller is not proven safe	1
Nothing new under the sum: A formal model of fast Fourier algorithms	1
Editorial Board	1
Editorial Board	1
A formal model for blockchain-based consent management in data sharing	1
Lifted structural invariant analysis of Petri net product lines	0
A tribute to José Manuel Valença	0
Operationally-based program equivalence proofs using LCTRSs	0
The correctness of concurrencies in (reversible) concurrent calculi	0
Finitely defined preference and preference indiscernibility in ATL with strategy contexts	0
Bridging formal methods and machine learning with model checking and global optimisation	0
Preface to selected papers from 20th Workshop on Programming and Languages (PROLE 2021)	0
Runtime monitoring of 5G network slicing using STAn	0
Preface to Rewriting Logic and Its Applications (revised selected papers from WRLA 2020)	0
Preface to selected papers from 22nd Workshop on Programming and Languages (PROLE 2023)	0
An axiomatic approach to differentiation of polynomial circuits	0
Editorial Board	0
Controlling stormwater detention ponds under partial observability	0
Verification of data-aware process models: Checking soundness of data Petri nets	0
A computational framework based on the dynamic pipeline approach	0
Specification and modelling of computing systems through graphs and graph transformation	0
Graph rewriting and relabeling with PBPO+: A unifying theory for quasitoposes	0
Safety enforcement via programmable strategies in Maude	0
Towards an efficient implementation of a tableau method for reactive safety specifications	0
Preface to the special issue on Open Problems in Concurrency Theory	0
Regular planar monoidal languages	0
NWPT 2022 - Special issue	0
Efficient iterative programs with distributed data collections	0
The Maude strategy language	0
Editorial Board	0
Partial arithmetical data types of rational numbers and their equational specification	0
Towards a type-based abstract semantics for Python	0
A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems	0
A logical approach to graph databases	0
Multiparty half-duplex systems and synchronous communications	0
Stone dualities from opfibrations	0
Fundamentals of compositional rewriting theory	0
Executable contracts for Elixir	0
Formal definitions and proofs for partial (co)recursive functions	0
Editorial Board	0
Compositional equivalences based on open pNets	0
Succinct ordering and aggregation constraints in algebraic array theories	0
Gaining trust by tracing security protocols	0
Specification of systems with parameterised events: An institution-independent approach	0
Computational category-theoretic rewriting	0
Formal lumping of polynomial differential equations through approximate equivalences	0
Hardware Trojan detection via rewriting logic	0
On the expressiveness and efficiency of guarded lists in Bach	0
Business processes resource management using rewriting logic and deep-learning-based predictive monitoring	0
Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms	0
Editorial Board	0
Formal reasoning about Bernstein-Vazirani algorithm	0
Combining sequential test cases into an equivalent set of adaptive test cases	0
Towards the exact complexity of realizability for Safety LTL	0
Branching pomsets: Design, expressiveness and applications to choreographies	0
A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3	0
A denotational semantics of Simulink with higher-order UTP	0
Computational modelling for combinatorial game strategies	0
Nominal anti-unification modulo equational theories	0
Certifying expressive power and algorithms of reversible primitive permutations with Lean	0

Preface to the special issue on the 12th Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES) 2020	0
Optimizing term rewriting with creeper trace transducers	0
Editorial Board	0
Variants and satisfiability in the infinitary unification wonderland	0
Formally verified animation for RoboChart using interaction trees	0
Formal analysis of real-time systems with user-defined strategies in rewriting logic	0
On algebraic array theories	0
Editorial Board	0
The generalised distribution semantics and projective families of distributions	0
Editorial Board	0
Liquidity analysis in resource-aware programming	0
Editorial Board	0
Unification of drags and confluence of drag rewriting	0
Makina: A QuickCheck state machine library	0
A formal semantics for agent distribution and fault tolerance in Jason	0
Determinism of multirelations	0
A semantic model for interacting cyber-physical systems	0
Comparing session type systems derived from linear logic	0
Composition of multilevel domain-specific modelling languages	0
Tuning similarity-based fuzzy logic programs	0
Formalization and analysis of the post-quantum signature scheme FALCON with Maude	0
Partially typed multiparty sessions with internal delegation	0
Evaluation diversity for graph conditions	0
Host-graph-sensitive RETE nets for incremental graph pattern matching with nested graph conditions	0
When causality meets fairness: A survey	0
Local confluence of conditional and generalized term rewriting systems	0
Editorial Board	0
Transforming concurrent programs with semaphores into logically constrained term rewrite systems	0
Kind inference for the FreeST programming language	0
Should computations halt?	0
A logical account of subtyping for session types	0
Editorial Board	0
Transforming orthogonal inductive definition sets into confluent term rewrite systems	0
Editorial Board	0
A rewriting logic semantics for the analysis of	0
Protocol choice and iteration for the free cornering	0
Editorial Board	0
The expression dependence graph	0
Control-data separation and logical condition propagation for efficient inference on probabilistic programs	0
Using fixed memory blocks in GPUs to accelerate SpMV multiplication in probabilistic model checkers	0
Corrigendum to “Runtime monitoring of 5G network slicing using STAn” [Journal of Logical and Algebraic Methods in Programming, 145 (2025) 101059]	0
Conceptual building blocks for modeling reconfiguration of component-based systems using Petri nets	0
Event structure semantics for multiparty sessions	0
Editorial Board	0
Reversible debugging of concurrent Erlang programs: Supporting imperative primitives	0
Processes against tests: On defining contextual equivalences	0