Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Keyword
-
- Linear Temporal Logic (3)
- Model Check (3)
- Operational Semantic (3)
- Label Transition System (2)
- Model Checker (2)
-
- Multitouch (2)
- Reinforcement learning (2)
- Sand animation (2)
- Tabletop computing (2)
- Access point (1)
- Activity pattern monitoring (1)
- Admissions (1)
- Agile development (1)
- Animation (1)
- Automated bug fixing (1)
- Automated detection (1)
- BDI architecture (1)
- Backlight Scaling (1)
- Behavior preservation (1)
- Binary tree formation (1)
- CSMA (1)
- CUDA (1)
- Character escaping (1)
- Code Vulnerabilities (1)
- Code search (1)
- Collaboration (1)
- Communication (1)
- Competition (1)
- Complexity Measures (1)
- Composite event monitoring (1)
Articles 1 - 30 of 49
Full-Text Articles in Physical Sciences and Mathematics
Case Study On Using A Programming Practice Tool For Evaluating University Applicants, Shannon Christopher Boesch, Kevin Steppe
Case Study On Using A Programming Practice Tool For Evaluating University Applicants, Shannon Christopher Boesch, Kevin Steppe
Research Collection School Of Computing and Information Systems
We used a programming practice tool to test basic programming skills of prospective students. A live competition was used to test those skills. Students who did well were asked for further interviews. Most students had no prior background and reported learning the basics of two programming languages within two weeks of self-study.
Automated Removal Of Cross Site Scripting Vulnerabilities In Web Applications, Lwin Khin Shar, Hee Beng Kuan Tan
Automated Removal Of Cross Site Scripting Vulnerabilities In Web Applications, Lwin Khin Shar, Hee Beng Kuan Tan
Research Collection School Of Computing and Information Systems
Context: Cross site scripting (XSS) vulnerability is among the top web application vulnerabilities according to recent surveys. This vulnerability occurs when a web application uses inputs received from users in web pages without properly checking them. This allows an attacker to inject malicious scripts in web pages via such inputs such that the scripts perform malicious actions when a client visits the exploited web pages. Such an attack may cause serious security violations such as account hijacking and cookie theft. Current approaches to mitigate this problem mainly focus on effective detection of XSS vulnerabilities in the programs or prevention of …
A Model Checking Framework For Hierarchical Systems., Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong
A Model Checking Framework For Hierarchical Systems., Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
BDD-based symbolic model checking is capable of verifying systems with a large number of states. In this work, we report an extensible framework to facilitate symbolic encoding and checking of hierarchical systems. Firstly, a novel library of symbolic encoding functions for compositional operators (e.g., parallel composition, sequential composition, choice operator, etc.) are developed so that users can apply symbolic model checking techniques to hierarchical systems with little knowledge of symbolic encoding techniques (like BDD or CUDD). Secondly, as the library is language-independent, we build an extensible framework with various symbolic model checking algorithms so that the library can be easily …
Search-Based Fault Localization, Shaowei Wang, David Lo, Lingxiao Jiang, - Lucia, Hoong Chuin Lau
Search-Based Fault Localization, Shaowei Wang, David Lo, Lingxiao Jiang, - Lucia, Hoong Chuin Lau
Research Collection School Of Computing and Information Systems
Many spectrum-based fault localization measures have been proposed in the literature. However, no single fault localization measure completely outperforms others: a measure which is more accurate in localizing some bugs in some programs is less accurate in localizing other bugs in other programs. This paper proposes to compose existing spectrum-based fault localization measures into an improved measure. We model the composition of various measures as an optimization problem and present a search-based approach to explore the space of many possible compositions and output a heuristically near optimal composite measure. We employ two search-based strategies including genetic algorithm and simulated annealing …
Towards Trajectory-Based Experience Sharing In A City, Byoungjip Kim, Youngki Lee, Sangjeong Lee, Yunseok Rhee, Junehwa Song
Towards Trajectory-Based Experience Sharing In A City, Byoungjip Kim, Youngki Lee, Sangjeong Lee, Yunseok Rhee, Junehwa Song
Research Collection School Of Computing and Information Systems
As location-aware mobile devices such as smartphones have now become prevalent, people are able to easily record their trajectories in daily lives. Such personal trajectories are a very promising means to share their daily life experiences, since important contextual information such as significant locations and activities can be extracted from the raw trajectories. In this paper, we propose MetroScope, a trajectory-based real-time and on-the-go experience sharing system in a metropolitan city. MetroScope allows people to share their daily life experiences through trajectories, and enables them to refer to other people's diverse and interesting experiences in a city. Eventually, MetroScope aims …
Enabling Gpu Acceleration With Messaging Middleware, Randall E. Duran, Li Zhang, Tom Hayhurst
Enabling Gpu Acceleration With Messaging Middleware, Randall E. Duran, Li Zhang, Tom Hayhurst
Research Collection School Of Computing and Information Systems
Graphics processing units (GPUs) offer great potential for accelerating processing for a wide range of scientific and business applications. However, complexities associated with using GPU technology have limited its use in applications. This paper reviews earlier approaches improving GPU accessibility, and explores how integration with middleware messaging technologies can further improve the accessibility and usability of GPU-enabled platforms. The results of a proof-of-concept integration between an open-source messaging middleware platform and a general-purpose GPU platform using the CUDA framework are presented. Additional applications of this technique are identified and discussed as potential areas for further research.
Software Process Evaluation: A Machine Learning Approach, Ning Chen, Steven C. H. Hoi, Xiaokui Xiao
Software Process Evaluation: A Machine Learning Approach, Ning Chen, Steven C. H. Hoi, Xiaokui Xiao
Research Collection School Of Computing and Information Systems
Software process evaluation is essential to improve software development and the quality of software products in an organization. Conventional approaches based on manual qualitative evaluations (e.g., artifacts inspection) are deficient in the sense that (i) they are time-consuming, (ii) they suffer from the authority constraints, and (iii) they are often subjective. To overcome these limitations, this paper presents a novel semi-automated approach to software process evaluation using machine learning techniques. In particular, we formulate the problem as a sequence classification task, which is solved by applying machine learning algorithms. Based on the framework, we define a new quantitative indicator to …
Pat 3: An Extensible Architecture For Building Multi-Domain Model Checkers, Yang Liu, Jun Sun, Jin Song Dong
Pat 3: An Extensible Architecture For Building Multi-Domain Model Checkers, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Model checking is emerging as an effective software verification method. Although it is desirable to have a dedicated model checker for each application domain, implementing one is rather challenging. In this work, we develop an extensible and integrated architecture in PAT3 (PAT version 3.*) to support the development of model checkers for wide range application domains. PAT3 adopts a layered design with an intermediate representation layer (IRL), which separates modeling languages from model checking algorithms so that the algorithms can be shared by different languages. IRL contains several common semantic models to support wide application domains, and builds both explicit …
Coping With Distance: An Empirical Study Of Communication On The Jazz Platform, Renuka Sindhgatta, Bikram Sengupta, Subhajit Datta
Coping With Distance: An Empirical Study Of Communication On The Jazz Platform, Renuka Sindhgatta, Bikram Sengupta, Subhajit Datta
Research Collection School Of Computing and Information Systems
Global software development - which is characterized by teams separated by physical distance and/or time-zone differences - has traditionally posed significant communication challenges. Often these have caused delays in completing tasks, or created misalignment across sites leading to re-work. In recent years, however, a new breed of development environments with rich collaboration features have emerged to facilitate cross-site work in distributed projects. In this paper we revisit the question "does distance matter?" in the context of IBM Jazz Platform -- a state-of-the-art collaborative development environment. We study the ecosystem of a large distributed team of around 300 members across 35 …
Finding Relevant Answers In Software Forums, Swapna Gottopati, David Lo, Jing Jiang
Finding Relevant Answers In Software Forums, Swapna Gottopati, David Lo, Jing Jiang
Research Collection School Of Computing and Information Systems
Online software forums provide a huge amount of valuable content. Developers and users often ask questions and receive answers from such forums. The availability of a vast amount of thread discussions in forums provides ample opportunities for knowledge acquisition and summarization. For a given search query, current search engines use traditional information retrieval approach to extract webpages containing relevant keywords. However, in software forums, often there are many threads containing similar keywords where each thread could contain a lot of posts as many as 1,000 or more. Manually finding relevant answers from these long threads is a painstaking task to …
Designing Low-Cost Mobile Websites For Libraries, Tiffini Travis, Chee Hsien Aaron (Zheng Zhixian) Tay
Designing Low-Cost Mobile Websites For Libraries, Tiffini Travis, Chee Hsien Aaron (Zheng Zhixian) Tay
Research Collection Library
As smartphone ownership rises, usage patterns are expanding. Libraries face an increasing demand for online content delivered in a mobile compatible format while being constrained by financial and staffing limitations. Solutions are readily available through free and low-cost products to create mobile web pages and existing design models from which to draw inspiration. Platform-specific apps can easily support the kinds of content most commonly delivered on library mobile pages: basic contact information and outbound links to the catalog, databases, and other resources. Two software platforms for creating simple pages were tested, the free software from WordPress with mobile detection formatting …
Recommending People In Developers' Collaboration Network, Didi Surian, Nian Liu, David Lo, Hanghang Tong, Ee Peng Lim, Christos Faloutsos
Recommending People In Developers' Collaboration Network, Didi Surian, Nian Liu, David Lo, Hanghang Tong, Ee Peng Lim, Christos Faloutsos
Research Collection School Of Computing and Information Systems
Many software developments involve collaborations of developers across the globe. This is true for both open-source and closed-source development efforts. Developers collaborate on different projects of various types. As with any other teamwork endeavors, finding compatibility among members in a development team is helpful towards the realization of the team’s goal. Compatible members tend to share similar programming style and naming strategy, communicate well with one another, etc. However, finding the right person to work with is not an easy task. In this work, we extract information available from Sourceforge.Net, the largest database of open source software, and build developer …
Concern Localization Using Information Retrieval: An Empirical Study On Linux Kernel, Shaowei Wang, David Lo, Zhenchang Xing, Lingxiao Jiang
Concern Localization Using Information Retrieval: An Empirical Study On Linux Kernel, Shaowei Wang, David Lo, Zhenchang Xing, Lingxiao Jiang
Research Collection School Of Computing and Information Systems
Many software maintenance activities need to find code units (functions, files, etc.) that implement a certain concern (features, bugs, etc.). To facilitate such activities, many approaches have been proposed to automatically link code units with concerns described in natural languages, which are termed as concern localization and often employ Information Retrieval (IR) techniques. There has not been a study that evaluates and compares the effectiveness of latest IR techniques on a large dataset. This study fills this gap by investigating ten IR techniques, some of which are new and have not been used for concern localization, on a Linux kernel …
An Efficient Algorithm For Learning Event-Recording Automata, Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, Yang Liu
An Efficient Algorithm For Learning Event-Recording Automata, Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, Yang Liu
Research Collection School Of Computing and Information Systems
In inference of untimed regular languages, given an unknown language to be inferred, an automaton is constructed to accept the unknown language from answers to a set of membership queries each of which asks whether a string is contained in the unknown language. One of the most well-known regular inference algorithms is the L* algorithm, proposed by Angluin in 1987, which can learn a minimal deterministic finite automaton (DFA) to accept the unknown language. In this work, we propose an efficient polynomial time learning algorithm, TL*, for timed regular language accepted by event-recording automata. Given an unknown timed regular language, …
Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li
Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li
Research Collection School Of Computing and Information Systems
Model Checking real-life systems is always difficult since such systems usually have quantitative timing factors and work in unreliable environment. The combination of real-time and probability in hierarchical systems presents a unique challenge to system modeling and analysis. In this work, we develop an automated approach for verifying probabilistic, real-time, hierarchical systems. Firstly, a modeling language called PRTS is defined, which combines data structures, real-time and probability. Next, a zone-based method is used to build a finite-state abstraction of PRTS models so that probabilistic model checking could be used to calculate the probability of a system satisfying certain property. We …
Cooperative Reinforcement Learning In Topology-Based Multi-Agent Systems, Dan Xiao, Ah-Hwee Tan
Cooperative Reinforcement Learning In Topology-Based Multi-Agent Systems, Dan Xiao, Ah-Hwee Tan
Research Collection School Of Computing and Information Systems
Topology-based multi-agent systems (TMAS), wherein agents interact with one another according to their spatial relationship in a network, are well suited for problems with topological constraints. In a TMAS system, however, each agent may have a different state space, which can be rather large. Consequently, traditional approaches to multi-agent cooperative learning may not be able to scale up with the complexity of the network topology. In this paper, we propose a cooperative learning strategy, under which autonomous agents are assembled in a binary tree formation (BTF). By constraining the interaction between agents, we effectively unify the state space of individual …
Code Search Via Topic-Enriched Dependence Graph Matching, Shaowei Wang, David Lo, Lingxiao Jiang
Code Search Via Topic-Enriched Dependence Graph Matching, Shaowei Wang, David Lo, Lingxiao Jiang
Research Collection School Of Computing and Information Systems
Source code contains textual, structural, and semantic information, which can all be leveraged for effective search. Some studies have proposed semantic code search where users can specify query topics in a natural language. Other studies can search through system dependence graphs. In this paper, we propose a semantic dependence search engine that integrates both kinds of techniques and can retrieve code snippets based on expressive user queries describing both topics and dependencies. Users can specify their search targets in a free form format describing desired topics (i.e., high-level semantic or functionality of the target code); a specialized graph query language …
Differencing Labeled Transition Systems, Zhenchang Xing, Jun Sun, Yang Liu, Jin Song Dong
Differencing Labeled Transition Systems, Zhenchang Xing, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Concurrent programs often use Labeled Transition Systems (LTSs) as their operational semantic models, which provide the basis for automatic system analysis and verification. System behaviors (generated from the operational semantics) evolve as programs evolve for fixing bugs or implementing new user requirements. Even when a program remains unchanged, its LTS models explored by a model checker or analyzer may be different due to the application of different exploration methods. In this paper, we introduce a novel approach (named SpecDiff) to computing the differences between two LTSs, representing the evolving behaviors of a concurrent program. SpecDiff considers LTSs as Typed Attributed …
A Survey Of Techniques And Challenges In Underwater Localization, Hwee-Pink Tan, Roee Diamant, Winston K. G. Seah, Marc Waldmeyer
A Survey Of Techniques And Challenges In Underwater Localization, Hwee-Pink Tan, Roee Diamant, Winston K. G. Seah, Marc Waldmeyer
Research Collection School Of Computing and Information Systems
Underwater Wireless Sensor Networks (UWSNs) are expected to support a variety of civilian and military applications. Sensed data can only be interpreted meaningfully when referenced to the location of the sensor, making localization an important problem. While global positioning system (GPS) receivers are commonly used in terrestrial WSNs to achieve this, this is infeasible in UWSNs as GPS signals do not propagate through water. Acoustic communications is the most promising mode of communication underwater. However, underwater acoustic channels are characterized by harsh physical layer conditions with low bandwidth, high propagation delay and high bit error rate. Moreover, the variable speed …
Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong
Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Orc is a computation orchestration language which is designed to specify computational services, such as distributed communication and data manipulation, in a concise and elegant way. Four concurrency primitives allow programmers to orchestrate site calls to achieve a goal, while managing timeouts, priorities, and failures. To guarantee the correctness of Orc model, effective verification support is desirable. Orc has a highly concurrent semantics which introduces the problem of state-explosion to search-based verification methods like model checking. In this paper, we present a new method, called Compositional Partial Order Reduction (CPOR), which aims to provide greater state-space reduction than classic partial …
Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu
Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu
Research Collection School Of Computing and Information Systems
Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. In this work, we present an automatic approach to directly verify WSNs built with TinyOS applications implemented in the NesC language. To achieve this target, we firstly define a set of formal operational semantics for most of the NesC language structures for the first time. This allows us to capture the behaviors of sensors by labelled transition systems (LTSs), which are the underlying semantic models of NesC programs. Secondly, WSNs are modeled …
Structural Complexity And Programmer Team Strategy: An Experimental Test, Narayan Ramasubbu, Chris F. Kemerer, Jeff Min Teck Hong
Structural Complexity And Programmer Team Strategy: An Experimental Test, Narayan Ramasubbu, Chris F. Kemerer, Jeff Min Teck Hong
Research Collection School Of Computing and Information Systems
This study develops and empirically tests the idea that the impact of structural complexity on perfective maintenance of object-oriented software is significantly determined by the team strategy of programmers (independent or collaborative). We analyzed two key dimensions of software structure, coupling and cohesion, with respect to the maintenance effort and the perceived ease-of-maintenance by pairs of programmers. Hypotheses based on the distributed cognition and task interdependence theoretical frameworks were tested using data collected from a controlled lab experiment employing professional programmers. The results show a significant interaction effect between coupling, cohesion, and programmer team strategy on both maintenance effort and …
Defending Against Cross Site Scripting Attacks, Lwin Khin Shar, Hee Beng Kuan Tan
Defending Against Cross Site Scripting Attacks, Lwin Khin Shar, Hee Beng Kuan Tan
Research Collection School Of Computing and Information Systems
Researchers have proposed multiple solutions to cross-site scripting, but vulnerabilities continue to exist in many Web applications due to developers' lack of understanding of the problem and their unfamiliarity with current defenses' strengths and limitations.
A Hybrid Agent Architecture Integrating Desire, Intention And Reinforcement Learning, Ah-Hwee Tan, Yew-Soon Ong, Akejariyawong Tapanuj
A Hybrid Agent Architecture Integrating Desire, Intention And Reinforcement Learning, Ah-Hwee Tan, Yew-Soon Ong, Akejariyawong Tapanuj
Research Collection School Of Computing and Information Systems
This paper presents a hybrid agent architecture that integrates the behaviours of BDI agents, specifically desire and intention, with a neural network based reinforcement learner known as Temporal DifferenceFusion Architecture for Learning and COgNition (TD-FALCON). With the explicit maintenance of goals, the agent performs reinforcement learning with the awareness of its objectives instead of relying on external reinforcement signals. More importantly, the intention module equips the hybrid architecture with deliberative planning capabilities, enabling the agent to purposefully maintain an agenda of actions to perform and reducing the need of constantly sensing the environment. Through reinforcement learning, plans can also be …
Automated Detection Of Likely Design Flaws In Layered Architectures, Aditya Budi, - Lucia, David Lo, Lingxiao Jiang, Shaowei Wang
Automated Detection Of Likely Design Flaws In Layered Architectures, Aditya Budi, - Lucia, David Lo, Lingxiao Jiang, Shaowei Wang
Research Collection School Of Computing and Information Systems
Layered architecture prescribes a good principle for separating concerns to make systems more maintainable. One example of such layered architectures is the separation of classes into three groups: Boundary, Control, and Entity, which are referred to as the three analysis class stereotypes in UML. Classes of different stereotypes are interacting with one another, when properly designed, the overall interaction would be maintainable, flexible, and robust. On the other hand, poor design would result in less maintainable system that is prone to errors. In many software projects, the stereotypes of classes are often missing, thus detection of design flaws becomes non-trivial. …
Real-Time Trip Information Service For A Large Taxi Fleet, Rajesh Krishna Balan, Nguyen Xuan Khoa, Lingxiao Jiang
Real-Time Trip Information Service For A Large Taxi Fleet, Rajesh Krishna Balan, Nguyen Xuan Khoa, Lingxiao Jiang
Research Collection School Of Computing and Information Systems
In this paper, we describe the design, analysis, implementation, and operational deployment of a real-time trip information system that provides passengers with the expected fare and trip duration of the taxi ride they are planning to take. This system was built in cooperation with a taxi operator that operates more than 15,000 taxis in Singapore. We first describe the overall system design and then explain the efficient algorithms used to achieve our predictions based on up to 21 months of historical data consisting of approximately 250 million paid taxi trips. We then describe various optimisations (involving region sizes, amount of …
Optimizing Sensor Data Acquisition For Energy-Efficient Smartphone-Based Continuous Event Processing, Archan Misra, Lipyeow Lim
Optimizing Sensor Data Acquisition For Energy-Efficient Smartphone-Based Continuous Event Processing, Archan Misra, Lipyeow Lim
Research Collection School Of Computing and Information Systems
Many pervasive applications, such as activity recognition or remote wellness monitoring, utilize a personal mobile device (aka smartphone) to perform continuous processing of data streams acquired from locally-connected, wearable, sensors. To ensure the continuous operation of such applications on a battery-limited mobile device, it is essential to dramatically reduce the energy overhead associated with the process of sensor data acquisition and processing. To achieve this goal, this paper introduces a technique of "acquisition-cost" aware continuous query processing, as part of the Acquisition Cost-Aware Query Adaptation (ACQUA) framework. ACQUA replaces the current paradigm, where the data is typically streamed (pushed) from …
Kb-Anonymity: A Model For Anonymized Behavior-Preserving Test And Debugging Data, Aditya Budi, David Lo, Lingxiao Jiang, Lucia Lucia
Kb-Anonymity: A Model For Anonymized Behavior-Preserving Test And Debugging Data, Aditya Budi, David Lo, Lingxiao Jiang, Lucia Lucia
Research Collection School Of Computing and Information Systems
It is often very expensive and practically infeasible to generate test cases that can exercise all possible program states in a program. This is especially true for a medium or large industrial system. In practice, industrial clients of the system often have a set of input data collected either before the system is built or after the deployment of a previous version of the system. Such data are highly valuable as they represent the operations that matter in a client's daily business and may be used to extensively test the system. However, such data often carries sensitive information and cannot …
High-Performance Composite Event Monitoring System Supporting Large Numbers Of Queries And Sources, Sangjeong Lee, Youngki Lee, Byoungjip Kim, K. Selcuk Candan, Yunseok Rhee, Junehwa Song
High-Performance Composite Event Monitoring System Supporting Large Numbers Of Queries And Sources, Sangjeong Lee, Youngki Lee, Byoungjip Kim, K. Selcuk Candan, Yunseok Rhee, Junehwa Song
Research Collection School Of Computing and Information Systems
This paper presents a novel data structure, called Event-centric Composable Queue (ECQ), a basic building block of a new scalable composite event monitoring (CEM) framework, SCEMon. In particular, we focus on the scalability issues when large numbers of CEM queries and event sources exist in upcoming CEM environments. To address these challenges effectively, we take an event-centric sharing approach rather than dealing with queries and sources separately. ECQ is a shared queue, which stores incoming event instances of a primitive event class. ECQs are designed to facilitate efficient shared evaluations of multiple queries over very large volumes of event streams …
On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong
On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Model checking has established itself as an effective system analysis method, as it is capable of proving/dis-proving properties automatically. Its application to practical systems is however limited by state space explosion. Among effective state reduction techniques are symmetry reduction and partial order reduction. Global fairness often plays a vital role in designing self-stabilizing population protocols. It is known that combining fairness and symmetry reduction is nontrivial. In this work, we first show that global fairness, unlike weak/strong fairness, can be combined with symmetry reduction. We extend the PAT model checker with the technique and demonstrate its usability by verifying recently …